Back to Search
Start Over
Certified Core-Guided MaxSAT Solving
- Source :
- 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 . Springer Science and Business Media Deutschland GmbH , Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) , vol. 14132 LNAI , pp. 1-22 , Proceedings of the 29th International Conference on Automated Deduction, CADE-29 , Rome , Italy , 01/07/2023 .
- Publication Year :
- 2023
-
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.
Details
- Database :
- OAIster
- Journal :
- 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 . Springer Science and Business Media Deutschland GmbH , Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) , vol. 14132 LNAI , pp. 1-22 , Proceedings of the 29th International Conference on Automated Deduction, CADE-29 , Rome , Italy , 01/07/2023 .
- Notes :
- application/pdf, English
- Publication Type :
- Electronic Resource
- Accession number :
- edsoai.on1439557316
- Document Type :
- Electronic Resource