Document Open Access Logo

Core-Guided Linear Programming-Based Maximum Satisfiability

Author George Katsirelos

PDF HTML 5

Files

Thumbnail PDF
PDF
LIPIcs.SAT.2025.17.pdf
  • Filesize: 0.83 MB
  • 17 pages
HTML5 Logo HTML (experimental)
LIPIcs.SAT.2025.17.html

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Discrete optimization
  • Mathematics of computing → Combinatorial optimization
  • Theory of computation → Logic
  • Mathematics of computing → Solvers
Keywords
  • maximum satisfiability
  • core-guided solvers
  • linear programming

Metrics

Abstract

The core-guided algorithm OLL is the basis of some of the most successful algorithms for MaxSAT in recent evaluations. It works by iteratively finding cores of the formula and transforming it so that it exhibits a higher lower bound. It has recently been shown to implicitly discover cores of the original formula, as well as a compact representation of its reasoning within a linear program. In this paper, we use and extend these results to design a practical MaxSAT solver. We show an explicit linear program which matches and usually exceeds the bound computed by OLL. We show that OLL can be restated as an algorithm that explicitly computes a feasible dual solution of this linear program. This restated algorithm naturally works with an arbitrary dual solution. It can in fact be used to improve any LP representation of the MaxSAT instance. This presents a large increase of the potential design space for such algorithms. We describe some potential improvements from this insight and show that an implementation outperforms the state of the art algorithms on the set of instances from the latest MaxSAT evaluation.

Cite As Get BibTex

George Katsirelos. Core-Guided Linear Programming-Based Maximum Satisfiability. In 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 341, pp. 17:1-17:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.SAT.2025.17

Author Details

George Katsirelos
  • Université Paris-Saclay, AgroParisTech, INRAE, UMR MIA Paris-Saclay, 91120, Palaiseau, France

Funding

Part of this work was funded by the AI Interdisciplinary Institute ANITI. ANITI is funded by the French "Investing for the Future – PIA3" program under the Grant agreement n°ANR-23-IACL-0002.

Supplementary Materials

References

  1. Benjamin Andres, Benjamin Kaufmann, Oliver Matheis, and Torsten Schaub. Unsatisfiability-based optimization in clasp. In Technical Communications of the 28th International Conference on Logic Programming (ICLP'12)(2012), pages 212-221. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2012. URL: https://doi.org/10.4230/LIPIcs.ICLP.2012.211.
  2. Carlos Ansótegui, Maria Luisa Bonet, Joel Gabàs, and Jordi Levy. Improving sat-based weighted maxsat solvers. In Michela Milano, editor, Principles and Practice of Constraint Programming - 18th International Conference, CP 2012, Québec City, QC, Canada, October 8-12, 2012. Proceedings, volume 7514 of Lecture Notes in Computer Science, pages 86-101. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-33558-7_9.
  3. Carlos Ansótegui, Maria Luisa Bonet, and Jordi Levy. Solving (weighted) partial maxsat through satisfiability testing. In International conference on theory and applications of satisfiability testing, pages 427-440. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-02777-2_39.
  4. Fahiem Bacchus, Antti Hyttinen, Matti Järvisalo, and Paul Saikko. Reduced cost fixing in maxsat. In J. Christopher Beck, editor, Principles and Practice of Constraint Programming - 23rd International Conference, CP 2017, Melbourne, VIC, Australia, August 28 - September 1, 2017, Proceedings, volume 10416 of Lecture Notes in Computer Science, pages 641-651. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-66158-2_41.
  5. Jeremias Berg, Fahiem Bacchus, and Alex Poole. Abstract cores in implicit hitting set maxsat solving. In Luca Pulina and Martina Seidl, editors, Theory and Applications of Satisfiability Testing - SAT 2020 - 23rd International Conference, Alghero, Italy, July 3-10, 2020, Proceedings, volume 12178 of Lecture Notes in Computer Science, pages 277-294. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-51825-7_20.
  6. Jeremias Berg, Bart Bogaerts, Jakob Nordström, Andy Oertel, and Dieter Vandesande. Certified core-guided MaxSAT solving. In Proceedings of the 29th International Conference on Automated Deduction (CADE-29), volume 14132 of Lecture Notes in Computer Science, pages 1-22, 2023. URL: https://doi.org/10.1007/978-3-031-38499-8_1.
  7. Suresh Bolusani, Mathieu Besançon, Ksenia Bestuzheva, Antonia Chmiela, João Dionísio, Tim Donkiewicz, Jasper van Doornmalen, Leon Eifler, Mohammed Ghannam, Ambros Gleixner, Christoph Graczyk, Katrin Halbig, Ivo Hedtke, Alexander Hoen, Christopher Hojny, Rolf van der Hulst, Dominik Kamp, Thorsten Koch, Kevin Kofler, Jurgen Lentz, Julian Manns, Gioni Mexi, Erik Mühmer, Marc E. Pfetsch, Franziska Schlösser, Felipe Serrano, Yuji Shinano, Mark Turner, Stefan Vigerske, Dieter Weninger, and Lixing Xu. The SCIP Optimization Suite 9.0. Technical report, Optimization Online, February 2024. URL: https://optimization-online.org/2024/02/the-scip-optimization-suite-9-0/.
  8. Guillaume Claus, Hadrien Cambazard, and Vincent Jost. Arc-consistency and linear programming duality: an analysis of reduced cost based filtering, 2022. URL: https://doi.org/10.48550/arxiv.2207.10325.
  9. Jessica Davies and Fahiem Bacchus. Solving MAXSAT by solving a sequence of simpler SAT instances. In Jimmy Ho-Man Lee, editor, Principles and Practice of Constraint Programming - CP 2011 - 17th International Conference, CP 2011, Perugia, Italy, September 12-16, 2011. Proceedings, volume 6876 of Lecture Notes in Computer Science, pages 225-239. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-23786-7_19.
  10. Jessica Davies and Fahiem Bacchus. Exploiting the power of mip solvers in maxsat. In Matti Järvisalo and Allen Van Gelder, editors, Theory and Applications of Satisfiability Testing - SAT 2013 - 16th International Conference, Helsinki, Finland, July 8-12, 2013. Proceedings, volume 7962 of Lecture Notes in Computer Science, pages 166-181. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-39071-5_13.
  11. Jessica Davies and Fahiem Bacchus. Postponing optimization to speed up MAXSAT solving. In Christian Schulte, editor, Principles and Practice of Constraint Programming - 19th International Conference, CP 2013, Uppsala, Sweden, September 16-20, 2013. Proceedings, volume 8124 of Lecture Notes in Computer Science, pages 247-262. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-40627-0_21.
  12. Niklas Eén and Niklas Sörensson. Translating pseudo-boolean constraints into SAT. J. Satisf. Boolean Model. Comput., 2(1-4):1-26, 2006. URL: https://doi.org/10.3233/sat190014.
  13. Filippo Focacci, Andrea Lodi, and Michela Milano. Cost-based domain filtering. In Joxan Jaffar, editor, Principles and Practice of Constraint Programming - CP'99, 5th International Conference, Alexandria, Virginia, USA, October 11-14, 1999, Proceedings, volume 1713 of Lecture Notes in Computer Science, pages 189-203. Springer, 1999. URL: https://doi.org/10.1007/978-3-540-48085-3_14.
  14. Zhaohui Fu and Sharad Malik. On solving the partial MAX-SAT problem. In Armin Biere and Carla P. Gomes, editors, Theory and Applications of Satisfiability Testing - SAT 2006, 9th International Conference, Seattle, WA, USA, August 12-15, 2006, Proceedings, volume 4121 of Lecture Notes in Computer Science, pages 252-265. Springer, 2006. URL: https://doi.org/10.1007/11814948_25.
  15. Alexey Ignatiev, António Morgado, and João Marques-Silva. RC2: an efficient maxsat solver. J. Satisf. Boolean Model. Comput., 11(1):53-64, 2019. URL: https://doi.org/10.3233/SAT190116.
  16. Hannes Ihalainen, Jeremias Berg, and Matti Järvisalo. Unifying SAT-based approaches to maximum satisfiability solving. Journal of Artificial Intelligence Research, 2024. URL: https://doi.org/10.1613/jair.1.15986.
  17. George Katsirelos. An Analysis of Core-Guided Maximum Satisfiability Solvers Using Linear Programming. In Meena Mahajan and Friedrich Slivovsky, editors, 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023), volume 271 of Leibniz International Proceedings in Informatics (LIPIcs), pages 12:1-12:19, Dagstuhl, Germany, 2023. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.SAT.2023.12.
  18. Tuukka Korhonen, Jeremias Berg, Paul Saikko, and Matti Järvisalo. Clause redundancy and preprocessing in maximum satisfiability. In Serge Gaspers and Toby Walsh, editors, Proceedings of the 20th International Conference on Theory and Applications of Satisfiability Testing, (SAT '17), volume 10491 of Lecture Notes in Computer Science, pages 449-456. Springer, 2017. URL: https://doi.org/10.1007/978-3-031-10769-6_6.
  19. António Morgado, Carmine Dodaro, and João Marques-Silva. Core-guided maxsat with soft cardinality constraints. In Barry O'Sullivan, editor, Principles and Practice of Constraint Programming - 20th International Conference, CP 2014, Lyon, France, September 8-12, 2014. Proceedings, volume 8656 of Lecture Notes in Computer Science, pages 564-573. Springer, 2014. URL: https://doi.org/10.1007/978-3-319-10428-7_41.
  20. António Morgado, Alexey Ignatiev, and João Marques-Silva. MSCG: robust core-guided maxsat solving. J. Satisf. Boolean Model. Comput., 9(1):129-134, 2014. URL: https://doi.org/10.3233/sat190105.
  21. Nina Narodytska and Fahiem Bacchus. Maximum satisfiability using core-guided maxsat resolution. In Proceedings of the Twenty-Eighth AAAI Conference on Artificial Intelligence, July 27 -31, 2014, Québec City, Québec, Canada., pages 2717-2723, 2014. URL: https://doi.org/10.1609/aaai.v28i1.9124.
  22. Nina Narodytska and Nikolaj S. Bjørner. Analysis of core-guided maxsat using cores and correction sets. In Kuldeep S. Meel and Ofer Strichman, editors, 25th International Conference on Theory and Applications of Satisfiability Testing, SAT 2022, August 2-5, 2022, Haifa, Israel, volume 236 of LIPIcs, pages 26:1-26:20. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. URL: https://doi.org/10.4230/LIPIcs.SAT.2022.26.
  23. Shiwei Pan, Yiyuan Wang, Shaowei Cai, Jiangman Li, Wenbo Zhu, and Minghao Yin. CASHWMaxSAT-DisjCad: Solver description. Technical report, Department of Computer Science, University of Helsinki, Helsinki, 2024. URL: http://hdl.handle.net/10138/584878.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact