Abstract
We describe three original exact solvers for Partial Max-SAT: PMS, PMS-hard, and PMS-learning. PMS is a branch and bound solver which incorporates efficient data structures, a dynamic variable selection heuristic, inference rules which exploit the fact that some clauses are hard, and a good quality lower bound based on unit propagation. PMS-hard is built on top of PMS and incorporates clause learning only for hard clauses; this learning is similar to the learning incorporated into modern SAT solvers. PMS-learning is built on top of PMS-hard and incorporates learning on both hard and soft clauses; the learning on soft clauses is quite different from the learning on SAT since it has to use Max-SAT resolution instead of SAT resolution. Finally, we report on the experimental investigation in which we compare the state-of-the-art solvers Toolbar and ChaffBS with PMS, PMS-hard, and PMS-learning. The results obtained provide empirical evidence that Partial Max-SAT is a suitable formalism for representing and solving over-constrained problems, and that the learning techniques we have defined in this paper can give rise to substantial performance improvements.
Research partially supported by projects TIN2004-07933-C03-03 and TIN2006-15662-C02-02 funded by the Ministerio de Educación y Ciencia.
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
Alsinet, T., Manyà, F., Planes, J.: Improved exact solver for weighted Max-SAT. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol. 3569, pp. 371–377. Springer, Heidelberg (2005)
Argelich, J., Manyà, F.: Solving over-constrained problems with SAT technology. In: Bacchus, F., Walsh, T. (eds.) SAT 2005. LNCS, vol. 3569, pp. 1–15. Springer, Heidelberg (2005)
Argelich, J., Manyà, F.: Exact Max-SAT solvers for over-constrained problems. Journal of Heuristics 12(4–5), 375–392 (2006)
Argelich, J., Manyà, F.: Learning hard constraints in Max-SAT. In: Proceedings of the Workshop on Constraint Solving and Constraint Logic Porgramming, CSCLP-2006, Lisbon, Portugal, pp. 1–12 (2006)
Bansal, N., Raman, V.: Upper bounds for MaxSat: Further improved. In: Aggarwal, A.K., Pandu Rangan, C. (eds.) ISAAC 1999. LNCS, vol. 1741, pp. 247–260. Springer, Heidelberg (1999)
Bonet, M., Levy, J., Manyà, F.: A complete calculus for Max-SAT. In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol. 4121, pp. 240–251. Springer, Heidelberg (2006)
Bonet, M., Levy, J., Manyà, F.: Resolution for Max-SAT. Artificial Intelligence (2007), doi:10.1016/j.artint.2007.03.001.
Cha, B., et al.: Local search algorithms for partial MAXSAT. In: Proceedings of the 14th National Conference on Artificial Intelligence, AAAI’97, Providence, RI, USA, pp. 263–268. AAAI Press, Menlo Park (1997)
Fu, Z., Malik, S.: On solving the partial MAX-SAT problem. In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol. 4121, pp. 252–265. Springer, Heidelberg (2006)
Heinink, V., Seckington, M., van der Werf, F.: Experiments on Random 2-SoftSAT. Technical report, Delft University of Technology (2006)
Heras, F., Larrosa, J.: New inference rules for efficient Max-SAT solving. In: Proceedings of the National Conference on Artificial Intelligence, AAAI-2006, Boston, MA, USA, pp. 68–73 (2006)
Larrosa, J., Oliveras, A., Heras, F.: MiniMaxSat: A New Weighted Max-SAT Solver. In: Marques-Silva, J., Sakallah, K.A. (eds.) SAT 2007. LNCS, vol. 4501, pp. 41–55. Springer, Heidelberg (2007)
Jeroslow, R.G., Wang, J.: Solving propositional satisfiability problems. Annals of Mathematics and Artificial Intelligence 1, 167–187 (1990)
Jiang, Y., Kautz, H., Selman, B.: Solving problems with hard and soft constraints using a stochastic algorithm for MAX-SAT. In: Proceedings of the 1st International Workshop on Artificial Intelligence and Operations Research (1995)
Larrosa, J., Heras, F.: Resolution in Max-SAT and its relation to local consistency in weighted CSPs. In: Proceedings of the International Joint Conference on Artificial Intelligence, IJCAI-2005, Edinburgh, Scotland, pp. 193–198. Morgan Kaufmann, San Francisco (2005)
Li, C.M., Manyà, F., Planes, J.: Exploiting unit propagation to compute lower bounds in branch and bound Max-SAT solvers. In: van Beek, P. (ed.) CP 2005. LNCS, vol. 3709, pp. 403–414. Springer, Heidelberg (2005)
Li, C.M., Manyà, F., Planes, J.: Detecting disjoint inconsistent subformulas for computing lower bounds for Max-SAT. In: Proceedings of the 21st National Conference on Artificial Intelligence, AAAI-2006, Boston, MA, USA, pp. 86–91 (2006)
Loveland, D.W.: Automated Theorem Proving. A Logical Basis. Fundamental Studies in Computer Science, vol. 6. North-Holland, Amsterdam (1978)
Moskewicz, M., et al.: Chaff: Engineering an efficient sat solver. In: 39th Design Automation Conference (2001)
Shen, H., Zhang, H.: Study of lower bound functions for max-2-sat. In: Proceedings of AAAI-2004, pp. 185–190 (2004)
Xing, Z., Zhang, W.: An efficient exact algorithm for (weighted) maximum satisfiability. Artificial Intelligence 164(2), 47–80 (2005)
Zhang, L., et al.: Efficient conflict driven learning in a Boolean satisfiability solver. In: International Conference on Computer Aided Design, ICCAD-2001, San Jose, CA, USA, pp. 279–285 (2001)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer Berlin Heidelberg
About this paper
Cite this paper
Argelich, J., Manyà, F. (2007). Partial Max-SAT Solvers with Clause Learning. 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_7
Download citation
DOI: https://doi.org/10.1007/978-3-540-72788-0_7
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)