Certified Core-Guided MaxSAT Solving

Jeremias Berg; Bart Bogaerts; Jakob Nordström; Andy Oertel; Dieter Vandesande

doi:10.1007/978-3-031-38499-8_1

Certified Core-Guided MaxSAT Solving

Jeremias Berg, Bart Bogaerts, Jakob Nordström, Andy Oertel, Dieter Vandesande

Research output: Chapter in Book/Report/Conference proceeding › Conference paper › Research

12 Citations (Scopus)

48 Downloads (Pure)

Abstract

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
Publisher	Springer
Pages	1-22
Number of pages <span style="color:red"p> <font size="1.5"> ✽ </span> </font>	22
ISBN (Electronic)	978-3-031-38499-8
ISBN (Print)	978-3-031-38498-1
DOIs	https://doi.org/10.1007/978-3-031-38499-8_1
Publication status	Published - 2023
Event	29th International Conference on Automated Deduction - Rome, Italy Duration: 1 Jul 2023 → 4 Jul 2023

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	14132 LNAI
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	29th International Conference on Automated Deduction
Abbreviated title	CADE-29
Country/Territory	Italy
City	Rome
Period	1/07/23 → 4/07/23

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.

Publisher Copyright:
© 2023, The Author(s).

Access to Document

10.1007/978-3-031-38499-8_1

CertifiedCoreGuidedMaxSATAccepted author manuscript, 310 KB

Cite this

Berg, J., Bogaerts, B., Nordström, J., Oertel, A., & Vandesande, D. (2023). Certified Core-Guided MaxSAT Solving. In B. Pientka, & C. Tinelli (Eds.), Automated Deduction – CADE 29 - 29th International Conference on Automated Deduction, Proceedings (pp. 1-22). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 14132 LNAI). Springer. https://doi.org/10.1007/978-3-031-38499-8_1

Berg, Jeremias ; Bogaerts, Bart ; Nordström, Jakob ; Oertel, Andy ; Vandesande, Dieter. / Certified Core-Guided MaxSAT Solving. Automated Deduction – CADE 29 - 29th International Conference on Automated Deduction, Proceedings. editor / Brigitte Pientka ; Cesare Tinelli. Springer, 2023. pp. 1-22 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{892785a65f3a4fd78850548d20ea9178,

title = "Certified Core-Guided MaxSAT Solving",

abstract = "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.",

author = "Jeremias Berg and Bart Bogaerts and Jakob Nordstr{\"o}m and Andy Oertel and Dieter Vandesande",

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{\"o}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: {\textcopyright} 2023, The Author(s).; 29th International Conference on Automated Deduction, CADE-29 ; Conference date: 01-07-2023 Through 04-07-2023",

year = "2023",

doi = "10.1007/978-3-031-38499-8_1",

language = "English",

isbn = "978-3-031-38498-1",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer",

pages = "1--22",

editor = "Brigitte Pientka and Cesare Tinelli",

booktitle = "Automated Deduction – CADE 29 - 29th International Conference on Automated Deduction, Proceedings",

}

Berg, J, Bogaerts, B, Nordström, J, Oertel, A & Vandesande, D 2023, Certified Core-Guided MaxSAT Solving. in B Pientka & C Tinelli (eds), Automated Deduction – CADE 29 - 29th International Conference on Automated Deduction, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 14132 LNAI, Springer, pp. 1-22, 29th International Conference on Automated Deduction, Rome, Italy, 1/07/23. https://doi.org/10.1007/978-3-031-38499-8_1

Certified Core-Guided MaxSAT Solving. / Berg, Jeremias; Bogaerts, Bart; Nordström, Jakob; Oertel, Andy; Vandesande, Dieter.

Automated Deduction – CADE 29 - 29th International Conference on Automated Deduction, Proceedings. ed. / Brigitte Pientka; Cesare Tinelli. Springer, 2023. p. 1-22 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 14132 LNAI).

Research output: Chapter in Book/Report/Conference proceeding › Conference paper › Research

TY - GEN

T1 - Certified Core-Guided MaxSAT Solving

AU - Berg, Jeremias

AU - Bogaerts, Bart

AU - Nordström, Jakob

AU - Oertel, Andy

AU - Vandesande, Dieter

N1 - 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. Publisher Copyright: © 2023, The Author(s).

PY - 2023

Y1 - 2023

N2 - 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.

AB - 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.

UR - https://doi.org/10.1007/978-3-031-38499-8_1

UR - http://www.scopus.com/inward/record.url?scp=85172280951&partnerID=8YFLogxK

U2 - 10.1007/978-3-031-38499-8_1

DO - 10.1007/978-3-031-38499-8_1

M3 - Conference paper

SN - 978-3-031-38498-1

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 1

EP - 22

BT - Automated Deduction – CADE 29 - 29th International Conference on Automated Deduction, Proceedings

A2 - Pientka, Brigitte

A2 - Tinelli, Cesare

PB - Springer

T2 - 29th International Conference on Automated Deduction

Y2 - 1 July 2023 through 4 July 2023

ER -

Berg J, Bogaerts B, Nordström J, Oertel A, Vandesande D. Certified Core-Guided MaxSAT Solving. In Pientka B, Tinelli C, editors, Automated Deduction – CADE 29 - 29th International Conference on Automated Deduction, Proceedings. Springer. 2023. p. 1-22. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-031-38499-8_1

Certified Core-Guided MaxSAT Solving

Abstract

Publication series

Conference

Bibliographical note

Access to Document

Other files and links

Fingerprint

FWOAL1002: FRESCO: A FRamework for Explainable Solving and Constraint Optimization

Cite this

Certified Core-Guided MaxSAT Solving

Abstract

Publication series

Conference

Bibliographical note

Access to Document

Other files and links

Fingerprint

Projects

FWOAL1002: FRESCO: A FRamework for Explainable Solving and Constraint Optimization

Cite this