Abstract
The Maximum Satisfiability (MaxSAT) is the problem of determining the maximum number of clauses of a given Boolean formula in Conjunctive Normal Form (CNF) that can be satisfied by an assignment of truth values to the variables of the formula. Many exact solvers for MaxSAT have been developed during recent years, and many of them were presented in the well-known SAT Conference. Algorithms for MaxSAT generally fall into two categories: (1) branch and bound algorithms and (2) algorithms that use successive calls to a SAT solver (SAT-based), which this paper in on. In practical problems, SAT-based algorithms have been shown to be more efficient. This paper provides an experimental investigation to compare the performance of recent SAT-based and branch and bound algorithms on benchmarks of the MaxSAT Evaluations.
Keywords
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 subscriptionsReferences
Ansótegui, C., Bonet, M.L., Levy, J.: Solving (weighted) partial maxsat through satisfiability testing. In: Theory and Applications of Satisfiability Testing-SAT 2009, pp. 427–440 (2009)
Ansótegui, C., Bonet, M.L., Gabàs, J., Levy, J.: Improving sat-based weighted maxSAT solvers. In: Principles and Practice of Constraint Programming, pp. 86–101. Springer (2012)
Ansótegui, C., Bonet, M.L., Gabàs, J., Levy, J.: Improving WPM2 for (weighted) partial maxSAT. In: Principles and Practice of Constraint Programming, pp. 117–132. Springer (2013)
Ansótegui, C., Bonet, M.L., Levy, J.: A New Algorithm for Weighted Partial maxSAT (2010)
Ansótegui, C., Bonet, M.L., Levy, J.: SAT-based maxSAT algorithms. Artif. Intell. 196, 77–105 (2013)
Ansótegui, C., Malitsky, Y., Sellmann, M.: MaxSAT by Improved Instance-Specific Algorithm Configuration (2014)
Davies, J., Bacchus, F.: Postponing optimization to speed up maxSAT solving. In: Principles and Practice of Constraint Programming, pp. 247–262. Springer (2013)
Eén, N., Sörensson, N.: Translating pseudo-Boolean constraints into SAT. JSAT 2(1–4), 1–26 (2006)
Fu, Z., Malik, S.: On solving the partial MAX-SAT problem. In: Theory and Applications of Satisfiability Testing-SAT 2006, pp. 252–265 (2006)
Gent, I.P.: Arc consistency in sat. In: ECAI, vol. 2, pp. 121–125 (2002)
Heras, F., Morgado, A., Marques-Silva, J.: Core-guided binary search algorithms for maximum satisfiability. In: Proceedings of the AAAI National Conference (AAAI) (2011)
Koshimura, M., Zhang, T., Fujita, H., Hasegawa, R.: QMaxSAT: a partial Max-SAT solver system description. J. Satisfiability Boolean Model. Comput. 8, 95–100 (2012)
Le Berre, D., Parrain, A.: The SAT4J library, release 2.2 system description. J. Satisfiability Boolean Model. Comput. 7, 59–64 (2010)
Li, C.M., Manyà, F., Mohamedou, N., Planes, J.: Exploiting cycle structures in Max-SAT. In: Theory and Applications of Satisfiability Testing-SAT 2009, pp. 467–480 (2009)
Marques-Silva, J.: The MSUNCORE MaxSAT solver. In: SAT 2009 Competitive Events Booklet: Preliminary Version, p. 151 (2009)
Marques-Silva, J., Planes, J.: On Using Unsatisfiability for Solving Maximum Satisfiability. arXiv preprint arXiv:0712.1097 (2007)
Marques-Silva, J., Planes, J.: Algorithms for maximum satisfiability using unsatisfiable cores. In: Proceedings of the Conference on Design, Automation and Test in Europe, pp. 408–413. ACM (2008)
Morgado, A., Heras, F., Liffiton, M., Planes, J., Marques-Silva, J.: Iterative and core-guided MaxSAT solving: a survey and assessment. Constraints 18(4), 478–534 (2013)
Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: engineering an efficient SAT solver. In: Proceedings of the 38th Annual Design Automation Conference, pp. 530–535. ACM (2001)
Prestwich, S.: Variable dependency in local search: Prevention is better than cure. In: Theory and Applications of Satisfiability Testing-SAT 2007, pp. 107–120. Springer (2007)
Prestwich, S.D.: CNF encodings. In: Handbook of Satisfiability, vol. 185, pp. 75–97 (2009)
Sinz, C.: Towards an optimal CNF encoding of Boolean cardinalityconstraints. In: Principles and Practice of Constraint Programming-CP 2005, pp. 827–831 (2005)
Acknowledgments
I would like to thank Dr. Hassan Aly (Department of Mathematics, Cairo University), Dr. Rasha Shaheen (Department of Mathematics, Cairo University) and Dr. Carlos Ansótegui (University of Lleida) for helping me throughout this research.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2018 Springer International Publishing AG
About this paper
Cite this paper
El Halaby, M. (2018). Solving MaxSAT by Successive Calls to a SAT Solver. In: Bi, Y., Kapoor, S., Bhatia, R. (eds) Proceedings of SAI Intelligent Systems Conference (IntelliSys) 2016. IntelliSys 2016. Lecture Notes in Networks and Systems, vol 15. Springer, Cham. https://doi.org/10.1007/978-3-319-56994-9_31
Download citation
DOI: https://doi.org/10.1007/978-3-319-56994-9_31
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-56993-2
Online ISBN: 978-3-319-56994-9
eBook Packages: EngineeringEngineering (R0)