Abstract
An effective SAT preprocessing technique is the construction of symmetry breaking formulas: auxiliary clauses that guide a SAT solver away from needless exploration of symmetric subproblems. However, during the past decade, state-of-the-art SAT solvers rarely incorporated symmetry breaking. This suggests that the reduction of the search space does not outweigh the overhead incurred by detecting symmetry and constructing symmetry breaking formulas. We investigate three methods to construct more effective symmetry breaking formulas. The first method simply improves the encoding of symmetry breaking formulas. The second detects special symmetry subgroups, for which complete symmetry breaking formulas exist. The third infers binary symmetry breaking clauses for a symmetry group as a whole rather than longer clauses for individual symmetries. We implement these methods in a symmetry breaking preprocessor, and verify their effectiveness on both hand-picked problems as well as the 2014 SAT competition benchmark set. Our experiments indicate that our symmetry breaking preprocessor improves the current state-of-the-art in static symmetry breaking for SAT and has a sufficiently low overhead to improve the performance of modern SAT solvers on hard combinatorial instances.
Keywords
- Symmetry Breaking Constraints
- Binary Clauses
- Compact Encoding
- Constraint Programming Context
- Stabilizer Chain
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsNotes
- 1.
Pronounced “Break it!”.
- 2.
We omit negative literals from the cycle notation, noting that a symmetry always commutes with negation.
- 3.
We again omit negative literals in cycle notation.
- 4.
In case two detected row interchangeability matrices overlap, it is not always possible to choose the order on the variables so that both are broken completely. In this case, one of the row interchangeability groups will only be broken partially.
- 5.
A small adaptation to Algorithm 2 ensures BreakID only selects smallest variables that are not permuted by a previously detected row interchangeability group.
References
Aloul, F., Ramani, A., Markov, I., Sakallah, K.: Solving difficult SAT instances in the presence of symmetry. In: Proceedings of the 39th Design Automation Conference, 2002, pp. 731–736 (2002)
Aloul, F.A., Markov, I.L., Sakallah, K.A.: Shatter: efficient symmetry-breaking for boolean satisfiability. In: Design Automation Conference, pp. 836–839 (2003)
Aloul, F.A., Sakallah, K.A., Markov, I.L.: Efficient symmetry breaking for Boolean satisfiability. IEEE Trans. Comput. 55(5), 549–558 (2006)
Audemard, G., Simon, L.: Predicting learnt clauses quality in modern SAT solvers. In: Boutilier, C. (ed.) IJCAI, pp. 399–404 (2009)
Balint, A., Belov, A., Heule, M.J., Järvisalo, M.: The 2013 international SAT competition (2013). satcompetition.org/2013
Crawford, J.M., Ginsberg, M.L., Luks, E.M., Roy, A.: Symmetry-breaking predicates for search problems. In: Principles of Knowledge Representation and Reasoning, pp. 148–159. Morgan Kaufmann (1996)
Devriendt, J., Bogaerts, B.: BreakID, a symmetry breaking preprocessor for SAT solvers (2015). bitbucket.org/krr/breakid
Devriendt, J., Bogaerts, B., Bruynooghe, M.: BreakIDGlucose: On the importance of row symmetry. In: Proceedings of the Fourth International Workshop on the Cross-Fertilization Between CSP and SAT (CSPSAT) (2014). http://lirias.kuleuven.be/handle/123456789/456639
Eén, N., Sörensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 502–518. Springer, Heidelberg (2004)
Flener, P., Frisch, A.M., Hnich, B., Kiziltan, Z., Miguel, I., Pearson, J., Walsh, T.: Breaking row and column symmetries in matrix models. In: Van Hentenryck, P. (ed.) CP 2002. LNCS, vol. 2470, pp. 462–477. Springer, Heidelberg (2002). http://dx.doi.org/10.1007/3-540-46135-3_31
The GAP Group: GAP - Groups, Algorithms, and Programming, Version 4.7.9 (2015). www.gap-system.org
Haken, A.: The intractability of resolution. Theor. Comput. Sci. 39, 297–308 (1985). http://www.sciencedirect.com/science/article/pii/0304397585901446. Third Conference on Foundations of Software Technology and Theoretical Computer Science
Jefferson, C., Petrie, K.E.: Automatic generation of constraints for partial symmetry breaking. In: Lee, J. (ed.) CP 2011. LNCS, vol. 6876, pp. 729–743. Springer, Heidelberg (2011). http://dx.doi.org/10.1007/978-3-642-23786-7_55
Junttila, T., Kaski, P.: Engineering an efficient canonical labeling tool for large and sparse graphs. In: Applegate, D., Brodal, G.S., Panario, D., Sedgewick, R. (eds.) Proceedings of the Ninth Workshop on Algorithm Engineering and Experiments and the Fourth Workshop on Analytic Algorithms and Combinatorics, pp. 135–149. SIAM (2007)
Katebi, H., Sakallah, K.A., Markov, I.L.: Symmetry and satisfiability: an update. In: Strichman, O., Szeider, S. (eds.) SAT 2010. LNCS, vol. 6175, pp. 113–127. Springer, Heidelberg (2010)
Lee, J.H.M., Li, J.: Increasing symmetry breaking by preserving target symmetries. In: Milano, M. (ed.) CP 2012. LNCS, vol. 7514, pp. 422–438. Springer, Heidelberg (2012). http://dx.doi.org/10.1007/978-3-642-33558-7_32
Lynce, I., Marques-Silva, J.: Breaking symmetries in SAT matrix models. In: Marques-Silva, J., Sakallah, K.A. (eds.) SAT 2007. LNCS, vol. 4501, pp. 22–27. Springer, Heidelberg (2007). http://dx.doi.org/10.1007/978-3-540-72788-0_6
McDonald, I., Smith, B.: Partial symmetry breaking. In: Van Hentenryck, P. (ed.) CP 2002. LNCS, vol. 2470, pp. 431–445. Springer, Heidelberg (2002). http://dx.doi.org/10.1007/3-540-46135-3_29
McKay, B.D., Piperno, A.: Practical graph isomorphism. J. Symbolic Comput. 60, 94–112 (2014). http://www.sciencedirect.com/science/article/pii/S0747717113001193
Puget, J.F.: Breaking symmetries in all-different problems. In: Proceedings of the 19th International Joint Conference on Artificial Intelligence, IJCAI 2005, pp. 272–277 (2005)
Sabharwal, A.: Symchaff: exploiting symmetry in a structure-aware satisfiability solver. Constraints 14(4), 478–505 (2009). http://dx.doi.org/10.1007/s10601-008-9060-1
Sakallah, K.A.: Symmetry and satisfiability. In: Biere, A., Heule, M.J.H., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability, vol. 185, pp. 289–338. IOS Press, Amsterdam (2009)
Schaafsma, B., Heule, M.J.H., van Maaren, H.: Dynamic symmetry breaking by simulating Zykov contraction. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol. 5584, pp. 223–236. Springer, Heidelberg (2009).http://dx.doi.org/10.1007/978-3-642-02777-2_22
Seress, Á.: Permutation Group Algorithms. Cambridge University Press (2003). cambridgeBooksOnline. http://dx.doi.org/10.1017/CBO9780511546549
Shlyakhter, I.: Generating effective symmetry-breaking predicates for search problems. Discrete Appl. Math. 155(12), 1539–1548 (2007). http://dx.doi.org/10.1016/j.dam.2005.10.018
Urquhart, A.: Hard examples for resolution. J. ACM 34(1), 209–219. http://doi.acm.org/10.1145/7531.8928
Walsh, T.: Symmetry breaking constraints: Recent results. CoRR abs/1204.3348 (2012)
Acknowledgement
This research was supported by the project GOA 13/010 Research Fund KU Leuven and projects G.0489.10, G.0357.12 and G.0922.13 of FWO (Research Foundation - Flanders). Bart Bogaerts is supported by the Finnish Center of Excellence in Computational Inference Research (COIN) funded by the Academy of Finland (grant #251170).
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer International Publishing Switzerland
About this paper
Cite this paper
Devriendt, J., Bogaerts, B., Bruynooghe, M., Denecker, M. (2016). Improved Static Symmetry Breaking for SAT. In: Creignou, N., Le Berre, D. (eds) Theory and Applications of Satisfiability Testing – SAT 2016. SAT 2016. Lecture Notes in Computer Science(), vol 9710. Springer, Cham. https://doi.org/10.1007/978-3-319-40970-2_8
Download citation
DOI: https://doi.org/10.1007/978-3-319-40970-2_8
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-40969-6
Online ISBN: 978-3-319-40970-2
eBook Packages: Computer ScienceComputer Science (R0)