Skip to main content
SpringerLink
Log in

Weight-Aware Core Extraction in SAT-Based MaxSAT Solving

  • Conference paper
  • First Online:
Principles and Practice of Constraint Programming (CP 2017)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 10416))

Abstract

Maximum satisfiability (MaxSAT) is today a competitive approach to tackling NP-hard optimization problems in a variety of AI and industrial domains. A great majority of the modern state-of-the-art MaxSAT solvers are core-guided, relying on a SAT solver to iteratively extract unsatisfiable cores of the soft clauses in the working formula and ruling out the found cores via adding cardinality constraints into the working formula until a solution is found. In this work we propose weight-aware core extraction (WCE) as a refinement to the current common approach of core-guided solvers. WCE integrates knowledge of soft clause weights into the core extraction process, and allows for delaying the addition of cardinality constraints into the working formula. We show that WCE noticeably improves in practice the performance of PMRES, one of the recent core-guided MaxSAT algorithms using soft cardinality constraints, and explain how the approach can be integrated into other core-guided algorithms.

Work supported by Academy of Finland (grants 251170 COIN, 276412, 284591); and DoCS Doctoral School in Computer Science and Research Funds of the University of Helsinki.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    In our implementation used in the experiments of this work, we use the slightly more sophisticated diversity heuristic [5] which attempts to balance the number of new soft clauses introduced and the amount that \(w_{\max }\) is decreased.

  2. 2.

    Unfortunately, we do not have access to the source code of MSCG.

  3. 3.

    Originally in [31] PMRES was formalized as a special case of the so-called MAXRES [19] rule; the specific special case is equivalent to the formalization of PMRES used here.

References

  1. Alviano, M., Dodaro, C., Ricca, F.: A MaxSAT algorithm using cardinality constraints of bounded size. In: Proceedings of IJCAI, pp. 2677–2683. AAAI Press (2015)

    Google Scholar 

  2. Andres, B., Kaufmann, B., Matheis, O., Schaub, T.: Unsatisfiability-based optimization in clasp. In: Proceedings of ICLP Technical Communications, LIPIcs, vol. 17, pp. 211–221. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2012)

    Google Scholar 

  3. 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). doi:10.1007/978-3-642-02777-2_39

    Chapter  Google Scholar 

  4. Ansótegui, C., Bonet, M., Levy, J.: SAT-based MaxSAT algorithms. Artif. Intell. 196, 77–105 (2013)

    Article  MathSciNet  MATH  Google Scholar 

  5. Ansótegui, C., Bonet, M.L., Gabàs, J., Levy, J.: Improving SAT-based weighted MaxSat solvers. In: Milano, M. (ed.) CP 2012. LNCS, pp. 86–101. Springer, Heidelberg (2012). doi:10.1007/978-3-642-33558-7_9

    Chapter  Google Scholar 

  6. Ansótegui, C., Didier, F., Gabàs, J.: Exploiting the structure of unsatisfiable cores in MaxSAT. In: Proceedings of IJCAI, pp. 283–289. AAAI Press (2015)

    Google Scholar 

  7. Ansótegui, C., Gabàs, J., Levy, J.: Exploiting subproblem optimization in SAT-based MaxSAT algorithms. J. Heuristics 22(1), 1–53 (2016)

    Article  MATH  Google Scholar 

  8. Argelich, J., Le Berre, D., Lynce, I., Marques-Silva, J., Rapicault, P.: Solving Linux upgradeability problems using Boolean optimization. In: Proceedings of LoCoCo. Electronic Proceedings in Theoretical Computer Science, vol. 29, pp. 11–22 (2010)

    Google Scholar 

  9. Argelich, J., Li, C.M., Manyà, F., Planes, J.: MaxSAT Evaluations. http://maxsat.ia.udl.cat/

  10. Audemard, G., Lagniez, J.-M., Simon, L.: Improving glucose for incremental SAT solving with assumptions: application to MUS extraction. In: Järvisalo, M., Van Gelder, A. (eds.) SAT 2013. LNCS, vol. 7962, pp. 309–317. Springer, Heidelberg (2013). doi:10.1007/978-3-642-39071-5_23

    Chapter  Google Scholar 

  11. Berg, J., Järvisalo, M., Malone, B.: Learning optimal bounded treewidth Bayesian networks via maximum satisfiability. In: Proceedings of AISTATS, JMLR Workshop and Conference Proceedings, vol. 33, pp. 86–95 (2014). JMLR.org

  12. Bjørner, N., Narodytska, N.: Maximum satisfiability using cores and correction sets. In: Proceedings of IJCAI, pp. 246–252. AAAI Press (2015)

    Google Scholar 

  13. Bunte, K., Järvisalo, M., Berg, J., Myllymäki, P., Peltonen, J., Kaski, S.: Optimal neighborhood preserving visualization by maximum satisfiability. In: Proceedings of AAAI, pp. 1694–1700. AAAI Press (2014)

    Google Scholar 

  14. Chen, Y., Safarpour, S., Marques-Silva, J., Veneris, A.: Automated design debugging with maximum satisfiability. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 29(11), 1804–1817 (2010)

    Article  Google Scholar 

  15. Davies, J., Bacchus, F.: Exploiting the power of MIP solvers in MaxSaT. In: Järvisalo, M., Van Gelder, A. (eds.) SAT 2013. LNCS, vol. 7962, pp. 166–181. Springer, Heidelberg (2013). doi:10.1007/978-3-642-39071-5_13

    Chapter  Google Scholar 

  16. 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). doi:10.1007/11814948_25

    Chapter  Google Scholar 

  17. Guerra, J., Lynce, I.: Reasoning over biological networks using maximum satisfiability. In: Milano, M. (ed.) CP 2012. LNCS, pp. 941–956. Springer, Heidelberg (2012). doi:10.1007/978-3-642-33558-7_67

    Chapter  Google Scholar 

  18. Heras, F., Morgado, A., Marques-Silva, J.: Lower bounds and upper bounds for MaxSAT. In: Hamadi, Y., Schoenauer, M. (eds.) LION 2012. LNCS, pp. 402–407. Springer, Heidelberg (2012). doi:10.1007/978-3-642-34413-8_35

    Chapter  Google Scholar 

  19. Larrosa, J., Heras, F.: Resolution in Max-SAT and its relation to local consistency in weighted CSPs. In: Proceedings of IJCAI, pp. 193–198. Professional Book Center (2005)

    Google Scholar 

  20. Li, C.M., Manyà, F., Mohamedou, N.O., Planes, J.: Resolution-based lower bounds in MaxSAT. Constraints 15(4), 456–484 (2010)

    Article  MathSciNet  MATH  Google Scholar 

  21. 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). doi:10.1007/11564751_31

    Chapter  Google Scholar 

  22. Li, C.M., Manyà, F., Planes, J.: Detecting disjoint inconsistent subformulas for computing lower bounds for Max-SAT. In: Proceedings of AAAI, pp. 86–91. AAAI Press (2006)

    Google Scholar 

  23. Lin, H., Su, K., Li, C.M.: Within-problem learning for efficient lower bound computation in Max-SAT solving. In: Proceedings of AAAI, pp. 351–356. AAAI Press (2008)

    Google Scholar 

  24. 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). doi:10.1007/978-3-642-02777-2_45

    Chapter  Google Scholar 

  25. Marques-Silva, J., Janota, M., Ignatiev, A., Morgado, A.: Efficient model based diagnosis with maximum satisfiability. In: Proceedings of IJCAI, pp. 1966–1972. AAAI Press (2015)

    Google Scholar 

  26. Marques-Silva, J., Argelich, J., Graça, A., Lynce, I.: Boolean lexicographic optimization: algorithms & applications. Ann. Math. Artif. Intell. 62(3–4), 317–343 (2011)

    Article  MathSciNet  MATH  Google Scholar 

  27. Marques-Silva, J., Planes, J.: On using unsatisfiability for solving maximum satisfiability. CoRR abs/0712.1097 (2007)

    Google Scholar 

  28. Martins, R., Joshi, S., Manquinho, V., Lynce, I.: Incremental cardinality constraints for MaxSAT. In: O’Sullivan, B. (ed.) CP 2014. LNCS, vol. 8656, pp. 531–548. Springer, Cham (2014). doi:10.1007/978-3-319-10428-7_39

    Google Scholar 

  29. Martins, R., Manquinho, V., Lynce, I.: Open-WBO: a modular MaxSAT solver’. In: Sinz, C., Egly, U. (eds.) SAT 2014. LNCS, vol. 8561, pp. 438–445. Springer, Cham (2014). doi:10.1007/978-3-319-09284-3_33

    Google Scholar 

  30. Morgado, A., Dodaro, C., Marques-Silva, J.: Core-guided MaxSAT with soft cardinality constraints. In: O’Sullivan, B. (ed.) CP 2014. LNCS, vol. 8656, pp. 564–573. Springer, Cham (2014). doi:10.1007/978-3-319-10428-7_41

    Google Scholar 

  31. Narodytska, N., Bacchus, F.: Maximum satisfiability using core-guided MaxSAT resolution. In: Proceedings of AAAI, pp. 2717–2723. AAAI Press (2014)

    Google Scholar 

  32. Saikko, P., Berg, J., Järvisalo, M.: LMHS: a SAT-IP hybrid MaxSAT solver. In: Creignou, N., Le Berre, D. (eds.) SAT 2016. LNCS, vol. 9710, pp. 539–546. Springer, Cham (2016). doi:10.1007/978-3-319-40970-2_34

    Google Scholar 

  33. Tseitin, G.S.: On the complexity of derivation in propositional calculus. In: Siekmann, J.H., Wrightson, G. (eds.) Automation of Reasoning. 2: Classical Papers on Computational Logic 1967–1970. Symbolic Computation, pp. 466–483. Springer, Heidelberg (1983)

    Chapter  Google Scholar 

  34. Zhu, C., Weissenbacher, G., Malik, S.: Post-silicon fault localisation using maximum satisfiability and backbones. In: Proceedings of FMCAD, pp. 63–66. FMCAD Inc. (2011)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. HIIT, Department of Computer Science, University of Helsinki, Helsinki, Finland

    Jeremias Berg & Matti Järvisalo

Authors
  1. Jeremias Berg
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Matti Järvisalo
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Jeremias Berg .

Editor information

Editors and Affiliations

  1. University of Toronto, Toronto, Ontario, Canada

    J. Christopher Beck

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG

About this paper

Cite this paper

Berg, J., Järvisalo, M. (2017). Weight-Aware Core Extraction in SAT-Based MaxSAT Solving. In: Beck, J. (eds) Principles and Practice of Constraint Programming. CP 2017. Lecture Notes in Computer Science(), vol 10416. Springer, Cham. https://doi.org/10.1007/978-3-319-66158-2_42

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-66158-2_42

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-66157-5

  • Online ISBN: 978-3-319-66158-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation