Shatter: efficient symmetry-breaking for boolean satisfiability

ABSTRACT

Boolean 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 remain difficult to solve [9] and continue to defy even the best available SAT solvers [5, 7]. Recent work pointed out that symmetries in the Boolean search space are often to blame. A theoretical framework for detecting and breaking such symmetries was introduced in [2]. This framework was subsequently extended, refined, and empirically shown to yield significant speed-ups for a large number of benchmark classes in [1].Symmetries in the search space are broken by adding appropriate symmetry-breaking predicates (SBPs) to a SAT instance in conjunctive normal form (CNF). The SBPs prune the search space by acting as a filter that confines the search to non-symmetric regions of the space without affecting the satisfiability of the CNF formula. For symmetry breaking to be effective in practice, the computational overhead of generating and manipulating the SBPs must be significantly less than the run time savings they yield due to search space pruning. In this paper we present several new constructions of SBPs that improve on previous work. Specifically, we give a linear-sized CNF formula that selects lex-leaders (among others) for single permutations. We also show how that formula can be simplified by taking advantage of the sparsity of permutations. We test these improvements against earlier constructions and show that they yield smaller SBPs and lead to run time reductions on many benchmarks.

REFERENCES

• 1: Fadi A. Aloul , Arathi Ramani , Igor L. Markov , Karem A. Sakallah, Solving difficult SAT instances in the presence of symmetry, Proceedings of the 39th conference on Design automation, June 10-14, 2002, New Orleans, Louisiana, USA [doi>10.1145/513918.514102]
• 2: J. Crawford, M. Ginsberg, E. Luks, and A. Roy, "Symmetry-breaking predicates for search problems," in Proc. of the Intl. Conference Principles of Knowledge Representation and Reasoning, 148--159, 1996.
• 3: DIMACS Challenge benchmarks in ftp://Dimacs.rutgers.EDU/pub/challenge/sat/benchmarks/cnf.
• 4: Ira M. Gessel , Richard P. Stanley, Algebraic enumeration, Handbook of combinatorics (vol. 2), MIT Press, Cambridge, MA, 1996
• 5: E. Goldberg , Y. Novikov, BerkMin: A Fast and Robust Sat-Solver, Proceedings of the conference on Design, automation and test in Europe, p.142, March 04-08, 2002
• 6: B. McKay, "Practical Graph Isomorphism," in Congressus Numerantium, vol. 30, 45--87, 1981.
• 7: 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]
• 8: Gi-Joon Nam , Fadi Aloul , Karem Sakallah , Rob Rutenbar, A comparative study of two Boolean formulations of FPGA detailed routing constraints, Proceedings of the 2001 international symposium on Physical design, p.222-227, April 01-04, 2001, Sonoma, California, United States [doi>10.1145/369691.369777]
• 9: SAT 2002 Competition, http://www.satlive.org/SATCompetition/submittedbenchs.html
• 10: 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]

INDEX TERMS

General Terms:
Algorithms, Experimentation, Verification

Keywords:
CNF, SAT, backtrack search, clause learning, graph automorphism, logic simplification, routing, symmetries