×

zbMATH — the first resource for mathematics

Exploiting cycle structures in Max-SAT. (English) Zbl 1247.68256
Kullmann, Oliver (ed.), Theory and applications of satisfiability testing – SAT 2009. 12th international conference, SAT 2009, Swansea, UK, June 30–July 3, 2009. Proceedings. Berlin: Springer (ISBN 978-3-642-02776-5/pbk). Lecture Notes in Computer Science 5584, 467-480 (2009).
Summary: We investigate the role of cycles structures (i.e., subsets of clauses of the form \(\bar{l}_{1}\vee l_{2}\), \(\bar{l}_{1}\vee l_{3}\), \(\bar{l}_{2}\vee\bar{l}_{3}\)) in the quality of the lower bound (LB) of modern MaxSAT solvers. Given a cycle structure, we have two options: (i) use the cycle structure just to detect inconsistent subformulas in the underestimation component, and (ii) replace the cycle structure with \(\bar{l}_{1}\), \(l_{1}\vee\bar{l}_{2}\vee\bar{l}_{3}\), \(\bar{l}_{1}\vee l_{2}\vee l_{3}\) by applying MaxSAT resolution and, at the same time, change the behaviour of the underestimation component. We first show that it is better to apply MaxSAT resolution to cycle structures occurring in inconsistent subformulas detected using unit propagation or failed literal detection. We then propose a heuristic that guides the application of MaxSAT resolution to cycle structures during failed literal detection, and evaluate this heuristic by implementing it in MaxSatz, obtaining a new solver called MaxSatz\(_{c }\). Our experiments on weighted MaxSAT and Partial MaxSAT instances indicate that MaxSatz\(_{c }\) substantially improves MaxSatz on many hard random, crafted and industrial instances.
For the entire collection see [Zbl 1165.68014].

MSC:
68T20 Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
Software:
MiniMaxSat
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Argelich, J., Li, C.M., Manyà, F.: An improved exact solver for partial Max-SAT. In: NCP 2007, pp. 230–231 (2007)
[2] Bonet, M.L., Levy, J., Manyà, F.: Resolution for Max-SAT. Artificial Intelligence 171(8-9), 240–251 (2007) · Zbl 1168.68541 · doi:10.1016/j.artint.2007.03.001
[3] Darras, S., Dequen, G., Devendeville, L., Li, C.M.: On inconsistent clause-subsets for max-SAT solving. In: Bessière, C. (ed.) CP 2007. LNCS, vol. 4741, pp. 225–240. Springer, Heidelberg (2007) · Zbl 1145.68509 · doi:10.1007/978-3-540-74970-7_18
[4] Heras, F., Larrosa, J., Oliveras, A.: 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) · Zbl 05527196 · doi:10.1007/978-3-540-72788-0_8
[5] Larrosa, J., Heras, F.: Resolution in Max-SAT and its relation to local consistency in weighted CSPs. In: IJCAI 2005, pp. 193–198 (2005) · Zbl 1153.68463
[6] Larrosa, J., Heras, F., de Givry, S.: A logical approach to efficient Max-SAT solving. Artificial Intelligence 172(2-3), 204–233 (2008) · Zbl 1182.68253 · doi:10.1016/j.artint.2007.05.006
[7] Li, C.M., Manyà, F., Mohamedou, N.O., Planes, J.: Transforming inconsistent subformulas in MaxSAT lower bound computation. In: Stuckey, P.J. (ed.) CP 2008. LNCS, vol. 5202, pp. 582–587. Springer, Heidelberg (2008) · Zbl 05372912 · doi:10.1007/978-3-540-85958-1_46
[8] 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) · Zbl 1153.68470 · doi:10.1007/11564751_31
[9] Li, C.M., Manyà, F., Planes, J.: Detecting disjoint inconsistent subformulas for computing lower bounds for Max-SAT. In: AAAI 2006, pp. 86–91 (2006)
[10] Li, C.M., Manyà, F., Planes, J.: New inference rules for Max-SAT. Journal of Artificial Intelligence Research 30, 321–359 (2007) · Zbl 1182.68254
[11] Lin, H., Su, K., Li, C.M.: Within-problem learning for efficient lower bound computation in Max-SAT solving. In: AAAI 2008, pp. 351–356 (2008)
[12] Pipatsrisawat, K., Darwiche, A.: Clone: Solving weighted Max-SAT in a reduced search space. In: AI 2007, pp. 223–233 (2007)
[13] Ramírez, M., Geffner, H.: Structural relaxations by variable renaming and their compilation for solving MinCostSAT. In: Bessière, C. (ed.) CP 2007. LNCS, vol. 4741, pp. 605–619. Springer, Heidelberg (2007) · Zbl 05318843 · doi:10.1007/978-3-540-74970-7_43
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.