Shatter v0.3

Identifies Symmetries in CNF Instances

Fadi A. Aloul, Igor L. Markov, Karem A. Sakallah

Introduction

• Shatter performs the following:
  - Reads a CNF formula as an input.
  - Detects the symmetries in the CNF formula using the graph automorphism tool SAUCY.
  (by Paul Darga at the University of Michigan - pdarga@umich.edu)
  - Augments the CNF instance with symmetry-breaking clauses and outputs it.
• General notes:
  - Used as a pre-processor.
  - Unsatisfiable instances will remain unsatisfiable.
  - Satisfiable instances will have fewer satisfying assignments, but given the symmetry-breaking clauses, it should be easy to extract the complete set of satisfying assignments of the original instance.

Example

Given the CNF formula:
p cnf 3 1
1 2 3 0

SymFind identifies two permutations, which generate the following symmetry-breaking clauses:
-2 3 0
-1 2 0

Download

• SHATTER, version 0.3, download the tarred, gzipped executable
• Intel/Linux - [Shatter_Linux_v03.tar.gz]
• Sun/Solaris - [Shatter_Solaris_v02.tar.gz]

• Other
• GAP/GRAPE: http://www-groups.dcs.st-andrews.ac.uk/~gap or http://www.gap-system.org
• SAUCY: http://vlsicad.eecs.umich.edu/BK/SAUCY
  
  

References

• F. Aloul, A. Ramani, I. Markov, and K. Sakallah, "Symmetry-Breaking for Pseudo-Boolean Formulas", ACM Journal of Experimental Algorithmics (JEA), vol. 12, article 1.3, 2007.
  
  
• F. Aloul, I. Markov, and K. Sakallah, "Efficient Symmetry-Breaking for Boolean Satisfiability", IEEE Transactions on Computers (TC), 55(5), pp. 549-558, May 2006.
  
  
• F. Aloul, A. Ramani, I. Markov, and K. Sakallah, "ShatterPB: Symmetry-Breaking for Pseudo-Boolean Formulas", Asia South Pacific Design Automation Conference (ASPDAC), Yokohama, Japan, pp. 884-887, 2004.
  
  
• F. Aloul, I. Markov, and K. Sakallah, "Efficient Symmetry-Breaking for Boolean Satisfiability", International Joint Conference on Artificial Intelligence (IJCAI), pp. 271-282, 2003.
  
  
• F. Aloul, I. Markov, and K. Sakallah, "Shatter: Efficient Symmetry-Breaking for Boolean Satisfiability", Design Automation Conference (DAC), pp. 836-839, 2003.
  
  
• F. Aloul, A. Ramani, I. Markov, and K. Sakallah, "Solving Difficult SAT Instances in the Presence of Symmetry", IEEE Transactions on Computer Aided Design, 22(9), pp. 1117-1137, 2003.
  
  
• F. Aloul, A. Ramani, I. Markov, and K. Sakallah, "Solving Difficult SAT Instances in the Presence of Symmetry", Design Automation Conference (DAC), pp. 731-736, 2002.

 

Maintained by Fadi Aloul (faloul@aus.edu)
Last updated September 1, 2009