Abstract
Maxsat is an optimization version of Satisfiability aimed at finding a truth assignment that maximizes the satisfaction of the theory. The technique of solving a sequence of SAT decision problems has been quite successful for solving larger, more industrially focused Maxsat instances, particularly when only a small number of clauses need to be falsified. The SAT decision problems, however, become more and more complicated as the minimal number of clauses that must be falsified increases. This can significantly degrade the performance of the approach. This technique also has more difficulty with the important generalization where each clause is given a weight: the weights generate SAT decision problems that are harder for SAT solvers to solve. In this paper we introduce a new Maxsat algorithm that avoids these problems. Our algorithm also solves a sequence of SAT instances. However, these SAT instances are always simplifications of the initial Maxsat formula, and thus are relatively easy for modern SAT solvers. This is accomplished by moving all of the arithmetic reasoning into a separate hitting set problem which can then be solved with techniques better suited to numeric reasoning, e.g., techniques from mathematical programming. As a result the performance of our algorithm is unaffected by the addition of clause weights. Our algorithm can, however, require solving more SAT instances than previous approaches. Nevertheless, the approach is simpler than previous methods and displays superior performance on some benchmarks.
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.
Similar content being viewed by others
References
Ansótegui, C., Bonet, M.L., Levy, J.: Solving (weighted) partial maxsat through satisfiability testing. In: Proceedings of Theory and Applications of Satisfiability Testing (SAT), pp. 427–440 (2009)
Ansótegui, C., Bonet, M.L., Levy, J.: A new algorithm for weighted partial maxsat. In: Proceedings of the AAAI National Conference (AAAI), pp. 3–8 (2010)
Argelich, J., Li, C.M., Manyà, F., Planes, J.: The First and Second Max-SAT Evaluations. JSAT 4(2-4), 251–278 (2008)
Berre, D.L., Parrain, A.: The sat4j library, release 2.2. JSAT 7(2-3), 56–59 (2010)
Davies, J., Cho, J., Bacchus, F.: Using learnt clauses in maxsat. In: Cohen, D. (ed.) CP 2010. LNCS, vol. 6308, pp. 176–190. Springer, Heidelberg (2010)
Fu, Z., Malik, S.: On solving the partial MAX-SAT problem. In: Theory and Applications of Satisfiability Testing (SAT), pp. 252–265 (2006)
Heras, F., Larrosa, J., Oliveras, A.: Minimaxsat: An efficient weighted max-sat solver. Journal of Artificial Intelligence Research (JAIR) 31, 1–32 (2008)
Kitching, M., Bacchus, F.: Exploiting decomposition in constraint optimization problems. In: Stuckey, P.J. (ed.) CP 2008. LNCS, vol. 5202, pp. 478–492. Springer, Heidelberg (2008)
Knuth, D.E.: Dancing links. In: Proceedings of the 1999 Oxford-Microsoft Symposium in Honour of Sir Tony Hoare, pp. 187–214. Palgrave, Oxford (2000)
Koshimura, M., Zhang, T.: Qmaxsat, http://sites.google.com/site/qmaxsat
Li, C.M., Manyà, F., Mohamedou, N.O., Planes, J.: Resolution-based lower bounds in maxsat. Constraints 15(4), 456–484 (2010)
Manquinho, V., Marques-Silva, J., Planes, J.: Algorithms for weighted boolean optimization. In: Proceedings of Theory and Applications of Satisfiability Testing (SAT), pp. 495–508 (2009)
Vazirani, V.: Approximation Algorithms. Springer, Heidelberg (2001)
Weihe, K.: Covering trains by stations or the power of data reduction. In: Proceedings of Algorithms and Experiments (ALEX 1998), pp. 1–8 (1998)
Wolsey, L.A.: Integer Programming. Wiley, Chichester (1998)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Davies, J., Bacchus, F. (2011). Solving MAXSAT by Solving a Sequence of Simpler SAT Instances. In: Lee, J. (eds) Principles and Practice of Constraint Programming – CP 2011. CP 2011. Lecture Notes in Computer Science, vol 6876. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-23786-7_19
Download citation
DOI: https://doi.org/10.1007/978-3-642-23786-7_19
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-23785-0
Online ISBN: 978-3-642-23786-7
eBook Packages: Computer ScienceComputer Science (R0)