Certified Core-Guided MaxSAT Solving
Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review
Documents
- Fulltext
Final published version, 566 KB, PDF document
In the last couple of decades, developments in SAT-based optimization have led to highly efficient maximum satisfiability (MaxSAT) solvers, but in contrast to the SAT solvers on which MaxSAT solving rests, there has been little parallel development of techniques to prove the correctness of MaxSAT results. We show how pseudo-Boolean proof logging can be used to certify state-of-the-art core-guided MaxSAT solving, including advanced techniques like structure sharing, weight-aware core extraction and hardening. Our experimental evaluation demonstrates that this approach is viable in practice. We are hopeful that this is the first step towards general proof logging techniques for MaxSAT solvers.
| Original language | English |
|---|---|
| Title of host publication | Automated Deduction – CADE 29 - 29th International Conference on Automated Deduction, Proceedings |
| Editors | Brigitte Pientka, Cesare Tinelli |
| Number of pages | 22 |
| Publisher | Springer Science and Business Media Deutschland GmbH |
| Publication date | 2023 |
| Pages | 1-22 |
| ISBN (Print) | 9783031384981 |
| DOIs | |
| Publication status | Published - 2023 |
| Event | Proceedings of the 29th International Conference on Automated Deduction, CADE-29 - Rome, Italy Duration: 1 Jul 2023 → 4 Jul 2023 |
Conference
| Conference | Proceedings of the 29th International Conference on Automated Deduction, CADE-29 |
|---|---|
| Land | Italy |
| By | Rome |
| Periode | 01/07/2023 → 04/07/2023 |
| Series | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |
|---|---|
| Volume | 14132 LNAI |
| ISSN | 0302-9743 |
Bibliographical note
Funding Information:
This work was partly carried out while some of the authors were visiting the Simons Institute for the Theory of Computing at UC Berkeley for the extended reunion of the program “Satisfiability: Theory, Practice, and Beyond” during the spring of 2023. We also benefited greatly from the Dagstuhl Seminar 22411 “Theory and Practice of SAT and Combinatorial Solving”. Additionally, we acknowledge several inspirational discussions on certifying solvers and proof logging with, among others, Ambros Gleixner, Stephan Gocht, and Ciaran McCreesh. The computational experiments were enabled by resources provided by LUNARC at Lund University. Jeremias Berg was fully supported by the Academy of Finland under grant 342145. Bart Bogaerts and Dieter Vandesande were supported by Fonds Wetenschappelijk Onderzoek – Vlaanderen (project G070521N) and by the EU ICT-48 2020 project TAI-LOR (GA 952215). Jakob Nordström was supported by the Swedish Research Council grant 2016-00782 and the Independent Research Fund Denmark grant 9040-00389B. Andy Oertel was supported by the Wallenberg AI, Autonomous Systems and Software Program (WASP) funded by the Knut and Alice Wallenberg Foundation.
Funding Information:
Jeremias Berg was fully supported by the Academy of Finland under grant 342145. Bart Bogaerts and Dieter Vandesande were supported by Fonds Wetenschappelijk Onderzoek – Vlaanderen (project G070521N) and by the EU ICT-48 2020 project TAILOR (GA 952215). Jakob Nordström was supported by the Swedish Research Council grant 2016-00782 and the Independent Research Fund Denmark grant 9040-00389B. Andy Oertel was supported by the Wallenberg AI, Autonomous Systems and Software Program (WASP) funded by the Knut and Alice Wallenberg Foundation.
Publisher Copyright:
© 2023, The Author(s).
- certifying algorithms, core-guided search, MaxSAT, proof logging
Research areas
ID: 390296710