Abstract
Recent research has focused on using the power of look-ahead to speed up the resolution of the Max-SAT problem. Indeed, look-ahead techniques such as Unit Propagation (UP) allow to find conflicts and to quickly reach the upper bound in a Branch-and-Bound algorithm, reducing the search-space of the resolution. In previous works, the Max-SAT solvers maxsatz9 and maxsatz14 use unit propagation to compute, at each node of the branch and bound search-tree, disjoint inconsistent subsets of clauses in the current subformula to estimate the minimum number of clauses that cannot be satisfied by any assignment extended from the current node. The same subsets may still be present in the subtrees, that is why we present in this paper a new method to memorize them and then spare their recomputation time. Furthermore, we propose a heuristic so that the memorized subsets of clauses induce an ordering among unit clauses to detect more inconsistent subsets of clauses. We show that this new approach improves maxsatz9 and maxsatz14 and suggest that the approach can also be used to improve other state-of-the-art Max-SAT solvers.
This work was partially supported by Région Champagne-Ardennes.
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
Watson, J., Beck, J., Howe, A., Whitley, L.: Toward an understanding of local search cost in job-shop scheduling (2001)
Iwama, K., Kambayashi, Y., Miyano, E.: New bounds for oblivious mesh routing. In: European Symposium on Algorithms, pp. 295–306 (1998)
Zhang, Y., Zha, H., Chao-Hsien, C., Ji, X., Chen, X.: Towards inferring protein interactions: Challenges and solutions. EURASIP Journal on Applied Signal Processing (2005)
Li, C.M., Manyà, F., Planes, J.: New inference rules for max-sat. Journal of Artificial Intelligence Research (to appear, 2007)
Heras, F., Larrosa, J.: New inference rules for efficient max-sat solving. In: AAAI (2006)
Lin, H., Su, K.: Exploiting inference rules to compute lower bounds for max-sat solving. In: IJCAI 2007 (2007)
Xing, Z., Zhang, W.: Maxsolver: an efficient exact algorithm for (weighted) maximum satisfiability. Artificial Intelligence 164(1-2), 47–80 (2005)
Larrosa, J., Schiex, T.: In the quest of the best form of local consistency for weighted csp. In: IJCAI, pp. 239–244 (2003)
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: AAAI, pp. 86–91 (2006)
Wallace, R., Freuder, E.: Comparative studies of constraint satisfaction and davis-putnam algorithms for maximum satisfiability problems. In: Cliques, Colouring and Satisfiability, pp. 587–615 (1996)
Wallace, R.J.: Directed arc consistency preprocessing. In: Constraint Processing, Selected Papers, pp. 121–137. Springer, London, UK (1995)
Larrosa, J., Meseguer, P., Schiex, T.: Maintaining reversible dac for max-csp. Artif. Intell. 107(1), 149–163 (1999)
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)
Shen, H., Zhang, H.: Study of lower bounds functions for max-2-sat. In: AAAI 2004, pp. 185–190 (2004)
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)
de Givry, S.: Singleton consistency and dominance for weighted csp. In: Wallace, M. (ed.) CP 2004. LNCS, vol. 3258. Springer, Heidelberg (2004)
Larrosa, J., Schiex, T.: In the quest of the best form of local consistency for weighted csp. In: IJCAI 2003 (2003)
Xing, Z., Zhang, W.: Maxsolver: an efficient exact algorithm for (weighted) maximum satisfiability. Artif. Intell. 164(1-2), 47–80 (2005)
Béjar, R., Manyà, F.: Solving combinatorial problems with regular local search algorithms. In: Ganzinger, H., McAllester, D., Voronkov, A. (eds.) LPAR 1999. LNCS, vol. 1705, pp. 33–43. Springer, Heidelberg (1999)
Béjar, R., Hähnle, R., Manyà, F.: A modular reduction of regular logic to classical logic. In: ISMVL 2001, pp. 221–226 (2001)
Ansótegui, C., Manyà, F.: Mapping problems with finite-domain variables into problems with boolean variables. In: Hoos, H.H., Mitchell, D.G. (eds.) SAT 2004. LNCS, vol. 3542, 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)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Darras, S., Dequen, G., Devendeville, L., Li, CM. (2007). On Inconsistent Clause-Subsets for Max-SAT Solving. In: Bessière, C. (eds) Principles and Practice of Constraint Programming – CP 2007. CP 2007. Lecture Notes in Computer Science, vol 4741. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-74970-7_18
Download citation
DOI: https://doi.org/10.1007/978-3-540-74970-7_18
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-74969-1
Online ISBN: 978-3-540-74970-7
eBook Packages: Computer ScienceComputer Science (R0)