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.
- Dimacs challenge benchmarks. Available at ftp://dimacs.rutgers.edu/pub/challenge/sat/benchmarks/cnf.Google Scholar
- A. V. Aho, J. E. Hopcroft, and J. D. Ullman. The Design and Analysis of Computer Algorithms. Addison-Wesley, 1974. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- F. A. Aloul, I. L. Markov, and K. A. Sakallah. Shatter: Efficient-symmetry breaking for boolean satisfiability. In Proceedings of the Design Automation Conference, pages 836--839, Anaheim, California, 2003. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- J. M. Crawford. A theoretical analysis of reasoning by symmetry in first-order logic. In AAAI Workshop on Tractable Reasoning, 1992.Google Scholar
- J. B. Fraleigh. A First Course in Abstract Algebra. Addison-Wesley, 6th edition, 1999.Google Scholar
- B. D. McKay. Backtrack programming and isomorph rejection on ordered subsets. Ars Combinatoria, 5:65--99, 1978.Google Scholar
- B. D. McKay. Practical graph isomorphism. Congressus Numerantium, 30:45--87, 1981.Google Scholar
- B. D. McKay. nauty user's guide (version 1.5). Technical Report TR-CS-90-02, Australian National University, Department of Computer Science, 1990.Google Scholar
- T. Miyazaki. The complexity of mckay's canonical labeling algorithm. In Groups and Computation II, pages 239--256, 1995.Google Scholar
- M. W. Moskewicz, C. F. Madigan, Y. Zhao, L. Zhang, and S. Malik. Chaff: Engineering an efficient SAT solver. In Proceedings of the Design Automation Conference, pages 530--535, 2001. Google ScholarDigital Library
- A. Urquhart. Hard examples for resolution. Journal of the ACM, 34(1):209--219, January 1987. Google ScholarDigital Library
- M. N. Velev and R. E. Bryant. Effective use of boolean satisfiability procedures in the formal verification of superscalar and VLIW microprocessors. In Proceedings of the Design Automation Conference, pages 226--231, 2001. Google ScholarDigital Library
- G. Wang, A. Kuehlmann, and A. Sangiovanni-Vincentelli. Structural detection of symmetries in boolean functions. In International Conference on Computer Design, pages 498--503, 2003. Google ScholarDigital Library
Index Terms
Exploiting structure in symmetry detection for CNF
Recommendations
Efficient Symmetry Breaking for Boolean Satisfiability
Identifying and breaking the symmetries of conjunctive normal form (CNF) formulae has been shown to lead to significant reductions in search times. Symmetries in the search space are broken by adding appropriate symmetry-breaking predicates (SBPs) to an ...
Shatter: efficient symmetry-breaking for boolean satisfiability
DAC '03: Proceedings of the 40th annual Design Automation ConferenceBoolean satisfiability (SAT) solvers have experienced dramatic improvements in their performance and scalability over the last several years [5, 7] and are now routinely used in diverse EDA applications. Nevertheless, a number of practical SAT instances ...
Solution and Optimization of Systems of Pseudo-Boolean Constraints
Optimized solvers for the Boolean Satisfiability (SAT) problem have many applications in areas such as hardware and software verification, FPGA routing, planning, etc. Further uses are complicated by the need to express "counting constraints" in ...
Comments