Abstract
maxsat is an optimization version of SAT capable of expressing a variety of practical problems. maxsat solvers have been designed to take advantage of many of the successful techniques of SAT solvers. However, the most important technique of modern SAT solvers, clause learning, has not been utilized since learnt clauses cannot be soundly added to a maxsat theory. In this paper we present a new method that allows SAT clause learning to be exploited in a maxsat solver without losing soundness. We present techniques for learning clauses during a branch and bound (B&B) maxsat search, a process that is more complicated than standard clause learning. To exploit these learnt clauses we develop a connection between them and bounds that can be used during B&B. This connection involves formulating a hitting set problem and finding bounds on its optimal solution. We present some new techniques for generating useful hitting set bounds and also show how linear and integer programs can be exploited for this purpose, opening the door for a hybrid approach to solving maxsat.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
References
Ansótegui, C., Bonet, M.L., Levy, J.: Solving (weighted) partial maxsat through satisfiability testing. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol. 5584, pp. 427–440. Springer, Heidelberg (2009)
Argelich, J., Li, C.M., Manyà, F., Planes, J.: The maxsat evaluations (2007–2009)
Bonet, M.L., 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)
Eén, N., Sörensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 502–518. Springer, Heidelberg (2004)
Freuder, E., Wallace, R.: Partial constraint satisfaction. Artificial Intelligence (AI) 58(1-3), 21–70 (1992)
de Givry, S., Larrosa, J., Meseguer, P., Schiex, T.: Solving max-SAT as weighted csp. In: Rossi, F. (ed.) CP 2003. LNCS, vol. 2833, pp. 363–376. Springer, Heidelberg (2003)
Heras, F., Larrosa, J., Oliveras, A.: MinimaxSAT: An efficient weighted max-sat solver. Journal of Artificial Intelligence Research (JAIR) 31, 1–32 (2008)
Kroc, L., Sabharwal, A., Selman, B.: Relaxed dpll search for maxsat. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol. 5584, pp. 447–452. Springer, Heidelberg (2009)
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 Artifical Intelligence (IJCAI). pp. 193–198 (2005)
Larrosa, J., Heras, F., de Givry, S.: A logical approach to efficient max-SAT solving. Artificial Intelligence (AI) 172(2-3), 204–233 (2008)
Li, C.M., Manyà, F., Mohamedou, N., Planes, J.: Exploiting cycle structures in max-SAT. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol. 5584, pp. 467–480. Springer, Heidelberg (2009)
Li, C.M., Manyà, F., Planes, J.: New inference rules for max-SAT. Journal of Artificial Intelligence Research (JAIR) 30, 321–359 (2007)
Liffiton, M., Sakallah, K.: Generalizing core-guided max-SAT. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol. 5584, pp. 481–494. Springer, Heidelberg (2009)
Manquinho, V., Marques-Silva, J., Planes, J.: Algorithms for weighted boolean optimization. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol. 5584, pp. 495–508. Springer, Heidelberg (2009)
Niedermeier, R., Rossmanith, P.: New upper bounds for maximum satisfiability. Journal of Algorithms 36, 63–88 (2000)
Petit, T., Bessière, C., Régin, J.C.: A general conflict-set based framework for partial constraint satisfaction. In: 5th Workshop on Soft Constraints (Soft 2003), Kinsale, Ireland (2003)
Schiex, T., Fargier, H., Verfaillie, G.: Valued constraint satisfaction problems: Hard and easy problems. In: Proceedings of the International Joint Conference on Artifical Intelligence (IJCAI), pp. 631–639 (1995)
Tompkins, D., Hoos, H.: Ubcsat: An implementation and experimentation environment for sls algorithms for SAT and max-SAT. In: Hoos, H., Mitchell, D.G. (eds.) SAT 2004. LNCS, vol. 3542, pp. 306–320. Springer, Heidelberg (2005)
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)
Xing, Z., Zhang, W.: Maxsolver: An efficient exact algorithm for (weighted) maximum satisfiability. Artificial Intelligence (AI) 164, 47–80 (2005)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Davies, J., Cho, J., Bacchus, F. (2010). Using Learnt Clauses in maxsat . In: Cohen, D. (eds) Principles and Practice of Constraint Programming – CP 2010. CP 2010. Lecture Notes in Computer Science, vol 6308. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-15396-9_17
Download citation
DOI: https://doi.org/10.1007/978-3-642-15396-9_17
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-15395-2
Online ISBN: 978-3-642-15396-9
eBook Packages: Computer ScienceComputer Science (R0)