Shatter v0.3

Identifies Symmetries in CNF Instances

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


  • 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 -
    - 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.


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




Maintained by Fadi Aloul (
Last updated September 1, 2009