Exploiting structure in symmetry detection for CNF

ABSTRACT

Instances of the Boolean satisfiability problem (SAT) arise in many areas of circuit design and verification. These instances are typically constructed from some human-designed artifact, and thus are likely to possess much inherent symmetry and sparsity. Previous work[4] has shown that exploiting symmetries results in vastly reduced SAT solver run times, often with the search for the symmetries themselves dominating the total SAT solving time. Our contribution is twofold. First, we dissect the algorithms behind the venerable NAUTY[9] package, particularly the partition refinement procedure responsible for the majority of search space pruning as well as the majority of run time overhead. Second, we present a new symmetry-detection tool, SAUCY, which outperforms NAUTY by several orders of magnitude on the large, structured CNF formulas generated from typical EDA problems.

REFERENCES

• 1: Dimacs challenge benchmarks. Available at ftp://dimacs.rutgers.edu/pub/challenge/sat/benchmarks/cnf.
• 2: Alfred V. Aho , John E. Hopcroft, The Design and Analysis of Computer Algorithms, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1974
• 3: F. A. Aloul, I. L. Markov, and K. A. Sakallah. Efficient symmetry breaking for boolean satisfiability. In Proceedings of the International Joint Conference on Artificial Intelligence, pages 271--282, Acapulco, Mexico, August 2003.
• 4: Fadi A. Aloul , Igor L. Markov , Karem A. Sakallah, Shatter: efficient symmetry-breaking for boolean satisfiability, Proceedings of the 40th conference on Design automation, June 02-06, 2003, Anaheim, CA, USA [doi>10.1145/775832.776042]
• 5: F. A. Aloul, A. Ramani, I. L. Markov, and K. A. Sakallah. Solving difficult instances of boolean satisfiability in the presence of symmetry. Transactions on Computer Aided Design, 22(9):1117--1137, 2003.
• 6: J. M. Crawford. A theoretical analysis of reasoning by symmetry in first-order logic. In AAAI Workshop on Tractable Reasoning, 1992.
• 7: J. B. Fraleigh. A First Course in Abstract Algebra. Addison-Wesley, 6th edition, 1999.
• 8: B. D. McKay. Backtrack programming and isomorph rejection on ordered subsets. Ars Combinatoria, 5:65--99, 1978.
• 9: B. D. McKay. Practical graph isomorphism. Congressus Numerantium, 30:45--87, 1981.
• 10: B. D. McKay. nauty user's guide (version 1.5). Technical Report TR-CS-90-02, Australian National University, Department of Computer Science, 1990.
• 11: T. Miyazaki. The complexity of mckay's canonical labeling algorithm. In Groups and Computation II, pages 239--256, 1995.
• 12: Matthew W. Moskewicz , Conor F. Madigan , Ying Zhao , Lintao Zhang , Sharad Malik, Chaff: engineering an efficient SAT solver, Proceedings of the 38th conference on Design automation, p.530-535, June 2001, Las Vegas, Nevada, United States [doi>10.1145/378239.379017]
• 13: Alasdair Urquhart, Hard examples for resolution, Journal of the ACM (JACM), v.34 n.1, p.209-219, Jan. 1987 [doi>10.1145/7531.8928]
• 14: Miroslav N. Velev , Randal E. Bryant, Effective use of boolean satisfiability procedures in the formal verification of superscalar and VLIW, Proceedings of the 38th conference on Design automation, p.226-231, June 2001, Las Vegas, Nevada, United States [doi>10.1145/378239.378469]
• 15: Guoqiang Wang , Andreas Kuehlmann , Alberto Sangiovanni-Vincentelli, Structural Detection of Symmetries in Boolean Functions, Proceedings of the 21st International Conference on Computer Design, p.498, October 13-15, 2003

INDEX TERMS

Primary Classification:
  G. Mathematics of Computing
  G.2 DISCRETE MATHEMATICS
      G.2.2 Graph Theory
          Subjects: Graph algorithms

General Terms:
Algorithms, Verification

Keywords:
abstract algebra, backtrack search, boolean satisfiability (SAT), graph automorphism, partition refinement, symmetry