Certified Core-Guided MaxSAT Solving
Berg, Jeremias ; Bogaerts, Bart ; Nordström, Jakob LU ; Oertel, Andy LU
and Vandesande, Dieter
(2023)
Proceedings of the 29th International Conference on Automated Deduction, CADE-29
In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
14132 LNAI.
p.1-22
- 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.
Please use this url to cite or link to this publication:
https://lup.lub.lu.se/record/72aeec8b-9135-44d9-b332-b51f212b2872
- author
- Berg, Jeremias
; Bogaerts, Bart
; Nordström, Jakob
LU
; Oertel, Andy
LU
and Vandesande, Dieter
- organization
- publishing date
- 2023
- type
- Chapter in Book/Report/Conference proceeding
- publication status
- published
- subject
- keywords
- certifying algorithms, core-guided search, MaxSAT, proof logging
- host publication
- Automated Deduction – CADE 29 - 29th International Conference on Automated Deduction, Proceedings
- series title
- Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
- editor
- Pientka, Brigitte and Tinelli, Cesare
- volume
- 14132 LNAI
- pages
- 22 pages
- publisher
- Springer Science and Business Media B.V.
- conference name
- Proceedings of the 29th International Conference on Automated Deduction, CADE-29
- conference location
- Rome, Italy
- conference dates
- 2023-07-01 - 2023-07-04
- external identifiers
-
- scopus:85172280951
- ISSN
- 1611-3349
- 0302-9743
- ISBN
- 9783031384981
- DOI
- 10.1007/978-3-031-38499-8_1
- language
- English
- LU publication?
- yes
- id
- 72aeec8b-9135-44d9-b332-b51f212b2872
- date added to LUP
- 2023-12-21 10:49:37
- date last changed
- 2024-04-19 20:22:07
@inproceedings{72aeec8b-9135-44d9-b332-b51f212b2872,
abstract = {{<p>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.</p>}},
author = {{Berg, Jeremias and Bogaerts, Bart and Nordström, Jakob and Oertel, Andy and Vandesande, Dieter}},
booktitle = {{Automated Deduction – CADE 29 - 29th International Conference on Automated Deduction, Proceedings}},
editor = {{Pientka, Brigitte and Tinelli, Cesare}},
isbn = {{9783031384981}},
issn = {{1611-3349}},
keywords = {{certifying algorithms; core-guided search; MaxSAT; proof logging}},
language = {{eng}},
pages = {{1--22}},
publisher = {{Springer Science and Business Media B.V.}},
series = {{Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)}},
title = {{Certified Core-Guided MaxSAT Solving}},
url = {{http://dx.doi.org/10.1007/978-3-031-38499-8_1}},
doi = {{10.1007/978-3-031-38499-8_1}},
volume = {{14132 LNAI}},
year = {{2023}},
}