SpringerLink
Log in

QMaxSATpb: A Certified MaxSAT Solver

  • Conference paper
  • First Online:
Logic Programming and Nonmonotonic Reasoning (LPNMR 2022)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 13416))

Abstract

While certification has been successful in the context of satisfiablity solving, with most state-of-the-art solvers now able to provide proofs of unsatisfiability, in maximum satisfiability, such techniques are not yet widespread. In this paper, we present QMaxSATpb, an extension of QMaxSAT that can produce proofs of optimality in the VeriPB proof format, which itself builds on the well-known cutting planes proof system. Our experiments demonstrate that proof logging is possible without much overhead.

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

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
EUR 32.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or Ebook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 59.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 79.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free ship** worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Similar content being viewed by others

Notes

  1. 1.

    Since QMaxSATpb is based on QMaxSAT version 0.1 [31], which does not support weights, we do not discuss weighted (partial) MaxSAT here. Later versions of QMaxSAT do support weights, using other encodings of PB constraints in CNF.

  2. 2.

    Here, we use the fact that we can assume that \(S=\{\overline{x_1},\dots ,\overline{x_n} \}\), but our proof logging and verification also work with an arbitrary set of soft clauses.

  3. 3.

    There, this rule was called substitution redundancy.

References

  1. Akgün, Ö., Gent, I.P., Jefferson, C., Miguel, I., Nightingale, P.: Metamorphic testing of constraint solvers. In: Proceedings of the 24th International Conference on Principles and Practice of Constraint Programming (CP 2018), pp. 727–736 (2018)

    Google Scholar 

  2. Alkassar, E., Böhme, S., Mehlhorn, K., Rizkallah, C., Schweitzer, P.: An introduction to certifying algorithms. it - Information Technology Methoden und innovative Anwendungen der Informatik und Informationstechnik 53(6), 287–293 (2011)

    Google Scholar 

  3. Alviano, M., Dodaro, C., Faber, W., Leone, N., Ricca, F.: WASP: a native ASP solver based on constraint learning. In: Cabalar, P., Son, T.C. (eds.) LPNMR 2013. LNCS (LNAI), vol. 8148, pp. 54–66. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-40564-8_6

    Chapter  Google Scholar 

  4. Avellaneda, F.: A short description of the solver EvalMaxSAT. In: MaxSAT Evaluation Solver and Benchmark Descriptions, pp. 10–11 (2021)

    Google Scholar 

  5. Bailleux, O., Boufkhad, Y.: Efficient CNF encoding of Boolean cardinality constraints. In: Rossi, F. (ed.) CP 2003. LNCS, vol. 2833, pp. 108–122. Springer, Heidelberg (2003). https://doi.org/10.1007/978-3-540-45193-8_8

    Chapter  MATH  Google Scholar 

  6. Biere, A.: Tracecheck (2006). http://fmv.jku.at/tracecheck/. Accessed 19 Mar 2021

  7. Bogaerts, B., Gocht, S., McCreesh, C., Nordström, J.: Certified symmetry and dominance breaking for combinatorial optimisation. In: Thirty-Sixth AAAI Conference on Artificial Intelligence, AAAI 2022, pp. 3698–3707. AAAI Press (2022). https://doi.org/10.1609/aaai.v36i4.20283

  8. Bonet, M.L., Levy, J., Manyà, F.: Resolution for Max-SAT. Artif. Intell. 171(8–9), 606–618 (2007)

    Article  MathSciNet  MATH  Google Scholar 

  9. Brummayer, R., Lonsing, F., Biere, A.: Automated testing and debugging of SAT and QBF solvers. In: Strichman, O., Szeider, S. (eds.) SAT 2010. LNCS, vol. 6175, pp. 44–57. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-14186-7_6

    Chapter  MATH  Google Scholar 

  10. Carnegie Mellon University, University of Helsinki, University of Toronto: The 2021 MaxSAT Evaluation (MSE 2021). https://maxsat-evaluations.github.io/2021/. Accessed June 2022

  11. Cook, W., Koch, T., Steffy, D.E., Wolter, K.: A hybrid branch-and-bound approach for exact rational mixed-integer programming. Math. Program. Comput. 5(3), 305–344 (2013)

    Article  MathSciNet  MATH  Google Scholar 

  12. Cook, W.J., Coullard, C.R., Turán, G.: On the complexity of cutting-plane proofs. Discret. Appl. Math. 18(1), 25–38 (1987)

    Article  MathSciNet  MATH  Google Scholar 

  13. Cruz-Filipe, L., Heule, M.J.H., Hunt, W.A., Kaufmann, M., Schneider-Kamp, P.: Efficient certified RAT verification. In: de Moura, L. (ed.) CADE 2017. LNCS (LNAI), vol. 10395, pp. 220–236. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-63046-5_14

    Chapter  Google Scholar 

  14. Cruz-Filipe, L., Marques-Silva, J., Schneider-Kamp, P.: Efficient certified resolution proof checking. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10205, pp. 118–135. Springer, Heidelberg (2017). https://doi.org/10.1007/978-3-662-54577-5_7

    Chapter  Google Scholar 

  15. De Cat, B., Bogaerts, B., Devriendt, J., Denecker, M.: Model expansion in the presence of function symbols using constraint programming. In: 2013 IEEE 25th International Conference on Tools with Artificial Intelligence (ICTAI 2013), pp. 1068–1075 (2013)

    Google Scholar 

  16. 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). https://doi.org/10.1007/978-3-540-24605-3_37

    Chapter  Google Scholar 

  17. Elffers, J., Gocht, S., McCreesh, C., Nordström, J.: Justifying all differences using pseudo-Boolean reasoning. In: Proceedings of the 34th AAAI Conference on Artificial Intelligence (AAAI 2020), pp. 1486–1494 (2020)

    Google Scholar 

  18. Fleury, M.: Formalization of logical calculi in Isabelle/HOL. Ph.D. thesis, Saarland University, Saarbrücken, Germany (2020)

    Google Scholar 

  19. Gebser, M., Kaufmann, B., Schaub, T.: Conflict-driven answer set solving: from theory to practice. Artif. Intell. 187, 52–89 (2012)

    Article  MathSciNet  MATH  Google Scholar 

  20. Gillard, X., Schaus, P., Deville, Y.: SolverCheck: declarative testing of constraints. In: Schiex, T., de Givry, S. (eds.) CP 2019. LNCS, vol. 11802, pp. 565–582. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-30048-7_33

    Chapter  Google Scholar 

  21. Gocht, S., Martins, R., Nordström, J., Oertel, A.: Certified CNF translations for pseudo-Boolean solving. In: Meel, K.S., Strichman, O. (eds.) 25th International Conference on Theory and Applications of Satisfiability Testing, (SAT ’22), pp. 16:1–16:25. Schloss Dagstuhl-Leibniz-Zentrum für Informatik (2022). https://doi.org/10.4230/LIPIcs.SAT.2022.16

  22. Gocht, S., McBride, R., McCreesh, C., Nordström, J., Prosser, P., Trimble, J.: Certifying solvers for clique and maximum common (connected) subgraph problems. In: Simonis, H. (ed.) CP 2020. LNCS, vol. 12333, pp. 338–357. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-58475-7_20

    Chapter  Google Scholar 

  23. Gocht, S., McCreesh, C., Nordström, J.: An auditable constraint programming solver. In: Solnon, C. (ed.) 28th International Conference on Principles and Practice of Constraint Programming, (CP’2022), pp. 25:1–25:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2022). https://doi.org/10.4230/LIPIcs.CP.2022.25

  24. Gocht, S., McCreesh, C., Nordström, J.: Subgraph isomorphism meets cutting planes: solving with certified solutions. In: Proceedings of the 29th International Joint Conference on Artificial Intelligence (IJCAI 2020), pp. 1134–1140 (2020)

    Google Scholar 

  25. Gocht, S., Nordström, J.: Certifying parity reasoning efficiently using pseudo-Boolean proofs. In: Proceedings of the 35th AAAI Conference on Artificial Intelligence (AAAI 2021), pp. 3768–3777 (2021)

    Google Scholar 

  26. Goldberg, E., Novikov, Y.: Verification of proofs of unsatisfiability for CNF formulas. In: Proceedings of the Conference on Design, Automation and Test in Europe (DATE 2003), pp. 886–891 (2003)

    Google Scholar 

  27. Heule, M.J.H., Hunt, W.A., Jr., Wetzler, N.: Trimming while checking clausal proofs. In: Proceedings of the 13th International Conference on Formal Methods in Computer-Aided Design (FMCAD 2013), pp. 181–188 (2013)

    Google Scholar 

  28. Heule, M.J.H., Hunt, W.A., Wetzler, N.: Verifying refutations with extended resolution. In: Bonacina, M.P. (ed.) CADE 2013. LNCS (LNAI), vol. 7898, pp. 345–359. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-38574-2_24

    Chapter  Google Scholar 

  29. Ignatiev, A., Morgado, A., Marques-Silva, J.: RC2: an efficient MaxSAT solver. J. Satisfiability Boolean Model. Comput. 11, 53–64 (2019)

    Google Scholar 

  30. Jahren, E., Achá, R.A.: The MSUSorting MaxSAT solver. In: MaxSAT Evaluation Solver and Benchmark Descriptions, p. 15 (2017)

    Google Scholar 

  31. Koshimura, M.: QMaxSAT: Q-dai MaxSAT solver. https://sites.google.com/site/qmaxsat/. Accessed June 2022

  32. Koshimura, M., Zhang, T., Fujita, H., Hasegawa, R.: QMaxSAT: a partial Max-SAT solver. J. Satisfiability Boolean Model. Comput. 8(1–2), 95–100 (2012). https://doi.org/10.3233/SAT190091

    Article  MathSciNet  MATH  Google Scholar 

  33. Larrosa, J., Nieuwenhuis, R., Oliveras, A., Rodríguez-Carbonell, E.: A framework for certified Boolean branch-and-bound optimization. J. Autom. Reason. 46(1), 81–102 (2011)

    Article  MathSciNet  MATH  Google Scholar 

  34. Manlove, D.F., O’Malley, G.: Paired and altruistic kidney donation in the UK: algorithms and experimentation. In: Proceedings of the 11th International Symposium on Experimental Algorithms (SEA 2012), pp. 271–282 (2012)

    Google Scholar 

  35. Marek, V., Truszczyński, M.: Stable models and an alternative logic programming paradigm. In: Apt, K.R., Marek, V., Truszczyński, M., Warren, D.S. (eds.) The Logic Programming Paradigm: A 25-Year Perspective, pp. 375–398. Springer, Heidelberg (1999). https://doi.org/10.1007/978-3-642-60085-2_17

  36. Marques Silva, J.P., Lynce, I., Malik, S.: Conflict-driven clause learning SAT solvers. In: Handbook of Satisfiability, pp. 131–153 (2009)

    Google Scholar 

  37. Martins, R., Terra-Neves, M., Joshi, S., Janota, M., Manquinho, V., Lynce, I.: Open-WBO in MaxSAT evaluation 2017. In: MaxSAT Evaluation Solver and Benchmark Descriptions, p. 17 (2017)

    Google Scholar 

  38. McConnell, R.M., Mehlhorn, K., Näher, S., Schweitzer, P.: Certifying algorithms. Comput. Sci. Rev. 5(2), 119–161 (2011)

    Article  MATH  Google Scholar 

  39. Morgado, A., Marques-Silva, J.: On validating Boolean optimizers. In: IEEE 23rd International Conference on Tools with Artificial Intelligence, ICTAI 2011, pp. 924–926 (2011)

    Google Scholar 

  40. Py, M., Cherif, M.S., Habet, D.: A proof builder for Max-SAT. In: Li, C.-M., Manyà, F. (eds.) SAT 2021. LNCS, vol. 12831, pp. 488–498. Springer, Cham (2021). https://doi.org/10.1007/978-3-030-80223-3_33

    Chapter  MATH  Google Scholar 

  41. Vandesande, D., De Wulf, W., Bogaerts, B.: QMaxSATpb: a certified MaxSAT solver. https://github.com/wulfdewolf/CertifiedMaxSAT. Accessed June 2022

  42. Vandesande, D., De Wulf, W., Bogaerts, B.: QMaxSATpb: a certified MaxSAT solver: patches & benchmarks. https://github.com/wulfdewolf/CertifiedMaxSAT_benchmarks. Accessed June 2022

  43. Wetzler, N., Heule, M.J.H., Hunt, W.A.: DRAT-trim: efficient checking and trimming using expressive clausal proofs. In: Sinz, C., Egly, U. (eds.) SAT 2014. LNCS, vol. 8561, pp. 422–429. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-09284-3_31

    Chapter  MATH  Google Scholar 

  44. Zhang, H.: Combinatorial designs by SAT solvers. In: Handbook of Satisfiability, pp. 533–568 (2009)

    Google Scholar 

Download references

Acknowledgement

The authors are grateful to Jeremias Berg, Stephan Gocht, Ciaran McCreesh, and Jakob Nordström for fruitful discussions on proof logging and feedback on previous versions of this manuscript. This work was partially supported by Fonds Wetenschappelijk Onderzoek – Vlaanderen (FWO) (project G070521N); computational resources and services were provided by the VSC (Flemish Supercomputer Center), funded by FWO and the Flemish Government.

Author information

Authors and Affiliations

  1. Artificial Intelligence Laboratory, Vrije Universiteit Brussel, Pleinlaan 9, 1050, Brussel, Belgium

    Dieter Vandesande, Wolf De Wulf & Bart Bogaerts

Authors
  1. Dieter Vandesande
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Wolf De Wulf
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Bart Bogaerts
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Dieter Vandesande .

Editor information

Editors and Affiliations

  1. University of Oxford, Oxford, UK

    Georg Gottlob

  2. Miami University, Oxford, OH, USA

    Daniela Inclezan

  3. University of Genova, Genoa, Italy

    Marco Maratea

Rights and permissions

Reprints and permissions

Copyright information

© 2022 The Author(s), under exclusive license to Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Vandesande, D., De Wulf, W., Bogaerts, B. (2022). QMaxSATpb: A Certified MaxSAT Solver. In: Gottlob, G., Inclezan, D., Maratea, M. (eds) Logic Programming and Nonmonotonic Reasoning. LPNMR 2022. Lecture Notes in Computer Science(), vol 13416. Springer, Cham. https://doi.org/10.1007/978-3-031-15707-3_33

Download citation

  • DOI: https://doi.org/10.1007/978-3-031-15707-3_33

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-031-15706-6

  • Online ISBN: 978-3-031-15707-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation