Abstract
Symmetry occurs naturally in many computational problems. The use of symmetry breaking techniques for solving search problems reduces the search space and therefore is expected to reduce the search time. Recent advances in breaking symmetries in SAT models are mainly focused on the identification of permutable variables via graph automorphism. These symmetries are denoted as instance-dependent, and although shown to be effective for different problem instances, the advantages of their generalised use in SAT are far from clear. Indeed, in many cases symmetry breaking predicates can introduce significant computational overhead, rendering ineffective the use of symmetry breaking. In contrast, in other domains, symmetry breaking is usually achieved by identifying instance-independent symmetries, often with promising experimental results. This paper studies the use of instance-independent symmetry breaking predicates in SAT. A concrete application is considered, and techniques for symmetry breaking in matrix models from CP are used. Our results indicate that instance-independent symmetry breaking predicates for matrix models can be significantly more effective than instance-dependent symmetry breaking predicates.
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 subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Aloul, F.A., et al.: Solving difficult instances in the presence of symmetry. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems 22(9), 1117–1137 (2003)
Crawford, J.M., et al.: Symmetry-breaking predicates for search problems. In: Proceedings of the International Conference on Principles of Knowledge Representation and Reasoning (1996)
Frisch, A.M., et al.: Breaking Row and Column Symmetries in Matrix Models. In: Van Hentenryck, P. (ed.) CP 2002. LNCS, vol. 2470, Springer, Heidelberg (2002)
Lynce, I., Marques-Silva, J.: Efficient haplotype inference with Boolean satisfiability. In: National Conference on Artificial Intelligence (AAAI) (2006)
Marques-Silva, J., Lynce, I.: SAT in Bioinformatics: Making the Case with Haplotype Inference. In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol. 4121, pp. 136–141. Springer, Heidelberg (2006)
Prestwich, S.: First-solution search with symmetry breaking and implied constraints. In: CP Workshop on Modelling and Problem Formulation (2001)
Ramani, A., et al.: Breaking instance-independent symmetries in exact graph coloring. Journal of Artificial Intelligence Research 26, 289–322 (2006)
Shlyakhter, I.: Generating effective symmetry-breaking predicates for search problems. In: LICS Workshop on Theory and Applications of Satisfiability Testing (2001)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer Berlin Heidelberg
About this paper
Cite this paper
Lynce, I., Marques-Silva, J. (2007). Breaking Symmetries in SAT Matrix Models. In: Marques-Silva, J., Sakallah, K.A. (eds) Theory and Applications of Satisfiability Testing – SAT 2007. SAT 2007. Lecture Notes in Computer Science, vol 4501. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-72788-0_6
Download citation
DOI: https://doi.org/10.1007/978-3-540-72788-0_6
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-72787-3
Online ISBN: 978-3-540-72788-0
eBook Packages: Computer ScienceComputer Science (R0)