This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Efficient Symmetry Breaking for Boolean Satisfiability
May 2006 (vol. 55 no. 5)
pp. 549-558
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 SAT instance in CNF. The SBPs prune the search space by acting as a filter that confines the search to nonsymmetric 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 SBPs must be significantly less than the runtime savings they yield due to search space pruning. In this paper, we describe a more systematic and efficient construction of SBPs. In particular, we use the cycle structure of symmetry generators, which typically involve very few variables, to drastically reduce the size of SBPs. Furthermore, our new SBP construction grows linearly with the number of relevant variables as opposed to the previous quadratic constructions. Our empirical data suggest that these improvements reduce search runtimes by one to two orders of magnitude on a wide variety of benchmarks with symmetries.

[1] F. Aloul, A. Ramani, I.L. Markov, and K. Sakallah, “Solving Difficult Instances of Boolean Satisfiability in the Presence of Symmetries,” IEEE Trans. Computer Aided Design, vol. 22, no. 9, pp. 1117-1137, 2003.
[2] F. Aloul, A. Ramani, I.L. Markov, and K. Sakallah, “Generic ILP versus Specialized 0-1 ILP,” Proc. Int'l Conf. Computer-Aided Design (ICCAD), pp. 450-457, 2002.
[3] R. Bayardo Jr. and R. Schrag, “Using CSP Look-Back Techniques to Solve Real World SAT Instances,” Proc. Nat'l Conf. Artificial Intelligence, pp. 203-208, 1997.
[4] A. Biere, A. Cimatti, E. Clarke, M. Fujita, and Y. Zhu, “Symbolic Model Checking Using SAT Procedures instead of BDDs,” Proc. Design Automation Conf. (DAC), pp. 317-320, 1999.
[5] J. Crawford, M. Ginsberg, E. Luks, and A. Roy, “Symmetry-Breaking Predicates for Search Problems,” Proc. Int'l Conf. Principles of Knowledge Representation and Reasoning, pp. 148-159, 1996.
[6] P. Darga, M.H. Liffiton, K.A. Sakallah, and I.L. Markov, “Exploiting Structure in Symmetry Generation for CNF,” Proc. Design Automation Conf. (DAC), pp. 530-534, 2004.
[7] DIMACS Challenge benchmarks, ftp://Dimacs.rutgers.EDU/pub/challenge/sat/ benchmarkscnf, 1996.
[8] N. Een and N. Sorensson, “An Extensible SAT-Solver,” Theory and Applications of Satisfiability Testing, pp. 502-518, 2003.
[9] J.B. Fraleigh, A First Course in Abstract Algebra, sixth ed. Reading, Mass.: Addison Wesley Longman, 2000.
[10] E. Goldberg and Y. Novikov, “BerkMin: A Fast and Robust SAT-Solver,” Proc. Design, Automation, and Test in Europe Conf. (DATE), pp. 142-149, 2002.
[11] T. Larrabee, “Test Pattern Generation Using Boolean Satisfiability,” IEEE Trans. Computer Aided Design, vol. 11, no. 1, pp. 4-15, 1992.
[12] B. McKay, “Practical Graph Isomorphism,” Congressus Numerantium, vol. 30, pp. 45-87, 1981, http://cs.anu.edu.au/bdmnauty/.
[13] M. Moskewicz, C. Madigan, Y. Zhao, L. Zhang, and S. Malik, “Chaff: Engineering an Efficient SAT Solver,” Proc. Design Automation Conf. (DAC), pp. 530-535, 2001.
[14] G. Nam, F. Aloul, K. Sakallah, and R. Rutenbar, “A Comparative Study of Two Boolean Formulations of FPGA Detailed Routing Constraints,” Proc. Int'l Symp. Physical Design (ISPD), pp. 222-227, 2001.
[15] S. Prestwich, “Supersymmetric Modeling for Local Search,” Proc. Workshop Symmetry and CSPs (SymCon), 2002.
[16] SAT 2002 Competition, http://www.satlive.org/SATCompetition submittedbenchs.html , 2002.
[17] B. Selman, H. Kautz, and B. Cohen, “Noise Strategies for Improving Local Search,” Proc. Nat'l Conf. Artificial Intelligence, pp. 337-343, 1994.
[18] J. Silva and K. Sakallah, “GRASP: A New Search Algorithm for Satisfiability,” IEEE Trans. Computers, vol. 48, no. 5, pp. 506-521, May 1999.
[19] E. Spitznagel, “Review of Mathematical Software, GAP,” Notices Am. Math. Soc., vol. 41, no. 7, pp. 780-782, 1994.
[20] P. Stephan, R. Brayton, and A. Sangiovanni-Vincentelli, “Combinational Test Generation Using Satisfiability,” IEEE Trans. Computer-Aided Design, vol. 15, no. 9, pp. 1167-1175, 1996.
[21] A. Urquhart, “Hard Examples for Resolution,” J. ACM, vol. 34, no. 1, pp. 209-219, 1987.
[22] M.N. Velev and R.E. Bryant, “Effective Use of Boolean Satisfiability Procedures in the Formal Verification of Superscalar and VLIW Microprocessors,” Proc. Design Automation Conf. (DAC), pp. 226-231, 2001.
[23] H. Zhang, “SATO: An Efficient Propositional Prover,” Proc. Int'l Conf. Automated Deduction, pp. 272-275, 1997.

Index Terms:
Backtrack Search, clause learning, conjunctive normal form (CNF), graph automorphism, satisfiability (SAT), symmetries.
Citation:
Fadi A. Aloul, Karem A. Sakallah, Igor L. Markov, "Efficient Symmetry Breaking for Boolean Satisfiability," IEEE Transactions on Computers, vol. 55, no. 5, pp. 549-558, May 2006, doi:10.1109/TC.2006.75
Usage of this product signifies your acceptance of the Terms of Use.