Abstract
Symmetries are intrinsic to many combinatorial problems including Boolean Satisfiability (SAT) and Constraint Programming (CP). In SAT, the identification of symmetry breaking predicates (SBPs) is a well-known, often effective, technique for solving hard problems. The identification of SBPs in SAT has been the subject of significant improvements in recent years, resulting in more compact SBPs and more effective algorithms. The identification of SBPs has also been applied to pseudo-Boolean (PB) constraints, showing that symmetry breaking can also be an effective technique for PB constraints. This paper extends further the application of SBPs, and shows that SBPs can be identified and used inMaximum Satisfiability (MaxSAT), as well as in its most well-known variants, including partial MaxSAT, weighted MaxSAT and weighted partial MaxSAT. As with SAT and PB, symmetry breaking predicates for MaxSAT and variants are shown to be effective for a representative number of problem domains, allowing solving problem instances that current state of the art MaxSAT solvers could not otherwise solve.
This paper extends a preliminary technical report [19] on the same subject.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Aloul, F., Sakallah, K.A., Markov, I.: Efficient symmetry breaking for boolean satisfiability. In: International Joint Conference on Artificial Intelligence, pp. 271–276 (August 2003)
Aloul, F.A., Ramani, A., Markov, I.L., Sakallah, K.A.: ShatterPB: symmetry-breaking for pseudo-Boolean formulas. In: Asian and South-Pacific Design Automation Conference, pp. 883–886 (2004)
Argelich, J., Li, C.M., Manyà, F., Planes, J.: MaxSAT evaluation (May 2007), www.maxsat07.udl.es
Benhamou, B., Sais, L.: Theoretical study of symmetries in propositional calculus and applications. In: Eleventh International Conference on Automated Deduction, pp. 281–294 (1992)
Borchers, B., Furman, J.: A two-phase exact algorithm for MAX-SAT and weighted MAX-SAT problems. Journal of Combinatorial Optimization 2(4), 299–306 (1998)
Cohen, D.A., Jeavons, P., Jefferson, C., Petrie, K.E., Smith, B.M.: Symmetry definitions for constraint satisfaction problems. In: International Conference on Principles and Practice of Constraint Programming, pp. 17–31 (2005)
Crawford, J.M., Ginsberg, M.L., Luks, E., Roy, A.: Symmetry-breaking predicates for search problems. In: International Conference on Principles of Knowledge Representation and Reasoning, pp. 148–159 (1996)
Darga, P.T., Liffiton, M.H., Sakallah, K.A., Markov, I.L.: Exploiting structure in symmetry detection for CNF. In: Design Automation Conference, pp. 530–534 (June 2004)
Darga, P.T., Sakallah, K.A., Markov, I.L.: Faster symmetry discovery using sparsity of symmetries. In: Design Automation Conference, pp. 149–154 (June 2008)
Gent, I.P., Kelsey, T., Linton, S., McDonald, I., Miguel, I., Smith, B.M.: Conditional symmetry breaking. In: International Conference on Principles and Practice of Constraint Programming, pp. 256–270 (2005)
Gent, I.P., Petrie, K.E., Puget, J.-F.: Symmetry in Constraint Programming. In: Handbook of Constraint Programming, pp. 329–376. Elsevier, Amsterdam (2006)
Gent, I.P., Smith, B.M.: Symmetry breaking in constraint programming. In: European Conference on Artificial Intelligence, pp. 599–603 (2000)
Heras, F., Larrosa, J.: New inference rules for efficient Max-SAT solving. In: AAAI Conference on Artificial Intelligence (2006)
Heras, F., Larrosa, J., Oliveras, A.: MiniMaxSat: a new weighted Max-SAT solver. In: International Conference on Theory and Applications of Satisfiability Testing, pp. 41–55 (May 2007)
Krishnamurthy, B.: Short proofs for tricky formulas. Acta Informatica 22(3), 253–275 (1985)
Li, C.M., Manyà, F., Planes, J.: Exploiting unit propagation to compute lower bounds in branch and bound Max-SAT solvers. In: International Conference on Principles and Practice of Constraint Programming, pp. 403–414 (2005)
Li, C.M., Manyà, F., Planes, J.: Detecting disjoint inconsistent subformulas for computing lower bounds for Max-SAT. In: AAAI Conference on Artificial Intelligence (July 2006)
Lin, H., Su, K.: Exploiting inference rules to compute lower bounds for MAX-SAT solving. In: International Joint Conference on Artificial Intelligence, pp. 2334–2339 (2007)
Marques-Silva, J., Lynce, I., Manquinho, V.: Symmetry breaking for maximum satisfiability. Computing Research Repository, abs/0804.0599 (April 2008), http://arxiv.org/abs/0804.0599
Marques-Silva, J., Manquinho, V.M.: Towards more effective unsatisfiability-based maximum satisfiability algorithms. In: International Conference on Theory and Applications of Satisfiability Testing, pp. 225–230 (2008)
Marques-Silva, J., Planes, J.: Algorithms for maximum satisfiability using unsatisfiable cores. In: Design, Automation and Testing in Europe Conference, pp. 408–413 (March 2008)
Puget, J.-F.: On the satisfiability of symmetrical constrained satisfaction problems. In: International Symposium on Methodologies for Intelligent Systems, pp. 350–361 (1993)
Smith, B.M.: Reducing symmetry in a combinatorial design problem. Technical Report 2001.01, School of Computing, University of Leeds (January 2001) (Presented at the CP-AI-OR Workshop April 2001)
Smith, B.M., Bistarelli, S., O’Sullivan, B.: Constraint symmetry for the soft CSP. In: International Conference on Principles and Practice of Constraint Programming, pp. 872–879 (September 2007)
Wallace, R., Freuder, E.: Comparative studies of constraint satisfaction and Davis-Putnam algorithms for maximum satisfiability problems. In: Johnson, D., Trick, M. (eds.) Cliques, Coloring and Satisfiability. DIMACS Series in Discrete Mathematics and Theoretical Computer Science, vol. 26, pp. 587–615. American Mathematical Society (1996)
Xing, Z., Zhang, W.: MaxSolver: An efficient exact algorithm for (weighted) maximum satisfiability. Artificial Intelligence 164(1-2), 47–80 (2005)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Marques-Silva, J., Lynce, I., Manquinho, V. (2008). Symmetry Breaking for Maximum Satisfiability. In: Cervesato, I., Veith, H., Voronkov, A. (eds) Logic for Programming, Artificial Intelligence, and Reasoning. LPAR 2008. Lecture Notes in Computer Science(), vol 5330. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-89439-1_1
Download citation
DOI: https://doi.org/10.1007/978-3-540-89439-1_1
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-89438-4
Online ISBN: 978-3-540-89439-1
eBook Packages: Computer ScienceComputer Science (R0)