Certified Core-Guided MaxSAT Solving

Publikation: Bidrag til bog/antologi/rapportKonferencebidrag i proceedingsForskningfagfællebedømt

Dokumenter

  • Fulltext

    Forlagets udgivne version, 566 KB, PDF-dokument

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.

OriginalsprogEngelsk
TitelAutomated Deduction – CADE 29 - 29th International Conference on Automated Deduction, Proceedings
RedaktørerBrigitte Pientka, Cesare Tinelli
Antal sider22
ForlagSpringer Science and Business Media Deutschland GmbH
Publikationsdato2023
Sider1-22
ISBN (Trykt)9783031384981
DOI
StatusUdgivet - 2023
BegivenhedProceedings of the 29th International Conference on Automated Deduction, CADE-29 - Rome, Italien
Varighed: 1 jul. 20234 jul. 2023

Konference

KonferenceProceedings of the 29th International Conference on Automated Deduction, CADE-29
LandItalien
ByRome
Periode01/07/202304/07/2023
NavnLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Vol/bind14132 LNAI
ISSN0302-9743

Bibliografisk note

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

ID: 390296710