Certified Core-Guided MaxSAT Solving

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

Onderzoeksoutput: Conference paper

31 Downloads (Pure)


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.

Originele taal-2English
TitelAutomated Deduction – CADE 29 - 29th International Conference on Automated Deduction, Proceedings
RedacteurenBrigitte Pientka, Cesare Tinelli
Aantal pagina's22
ISBN van elektronische versie978-3-031-38499-8
ISBN van geprinte versie978-3-031-38498-1
StatusPublished - 2023
Evenement29th International Conference on Automated Deduction - Rome, Italy
Duur: 1 jul 20234 jul 2023

Publicatie series

NaamLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume14132 LNAI
ISSN van geprinte versie0302-9743
ISSN van elektronische versie1611-3349


Conference29th International Conference on Automated Deduction
Verkorte titelCADE-29

Bibliografische nota

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


Duik in de onderzoeksthema's van 'Certified Core-Guided MaxSAT Solving'. Samen vormen ze een unieke vingerafdruk.

Citeer dit