Certified CNF Translations for Pseudo-Boolean Solving
Gocht, Stephan LU ; Martins, Ruben ; Nordström, Jakob LU and Oertel, Andy LU
(2022)
25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)
In Leibniz International Proceedings in Informatics (LIPIcs)
236.
- Abstract
- The dramatic improvements in Boolean satisfiability (SAT) solving since the turn of the millennium have made it possible to leverage state-of-the-art conflict-driven clause learning (CDCL) solvers for many combinatorial problems in academia and industry, and the use of proof logging has played a crucial role in increasing the confidence that the results these solvers produce are correct. However, the fact that SAT proof logging is performed in conjunctive normal form (CNF) clausal format means that it has not been possible to extend guarantees of correctness to the use of SAT solvers for more expressive combinatorial paradigms, where the first step is an unverified translation of the input to CNF.
In this work, we show how... (More) - The dramatic improvements in Boolean satisfiability (SAT) solving since the turn of the millennium have made it possible to leverage state-of-the-art conflict-driven clause learning (CDCL) solvers for many combinatorial problems in academia and industry, and the use of proof logging has played a crucial role in increasing the confidence that the results these solvers produce are correct. However, the fact that SAT proof logging is performed in conjunctive normal form (CNF) clausal format means that it has not been possible to extend guarantees of correctness to the use of SAT solvers for more expressive combinatorial paradigms, where the first step is an unverified translation of the input to CNF.
In this work, we show how cutting-planes-based reasoning can provide proof logging for solvers that translate pseudo-Boolean (a.k.a. 0-1 integer linear) decision problems to CNF and then run CDCL. To support a wide range of encodings, we provide a uniform and easily extensible framework for proof logging of CNF translations. We are hopeful that this is just a first step towards providing a unified proof logging approach that will also extend to maximum satisfiability (MaxSAT) solving and pseudo-Boolean optimization in general. (Less)
Please use this url to cite or link to this publication:
https://lup.lub.lu.se/record/49687a3e-73d1-4fbd-ab14-09073b3d86ab
- author
- Gocht, Stephan
LU
; Martins, Ruben
; Nordström, Jakob
LU
and Oertel, Andy
LU
- organization
- publishing date
- 2022-07-28
- type
- Chapter in Book/Report/Conference proceeding
- publication status
- published
- subject
- host publication
- 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)
- series title
- Leibniz International Proceedings in Informatics (LIPIcs)
- editor
- Meel, Kuldeep S. and Strichman, Ofer
- volume
- 236
- article number
- 16
- pages
- 25 pages
- publisher
- Schloss Dagstuhl - Leibniz-Zentrum für Informatik
- conference name
- 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)
- conference location
- Haifa, Israel
- conference dates
- 2022-08-02 - 2022-08-05
- external identifiers
-
- scopus:85136121900
- ISSN
- 1868-8969
- ISBN
- 978-3-95977-242-6
- DOI
- 10.4230/LIPIcs.SAT.2022.16
- project
- Certified Linear Pseudo-Boolean Optimization
- WASP: Wallenberg AI, Autonomous Systems and Software Program at Lund University
- language
- English
- LU publication?
- yes
- id
- 49687a3e-73d1-4fbd-ab14-09073b3d86ab
- alternative location
- https://drops.dagstuhl.de/opus/volltexte/2022/16690/pdf/LIPIcs-SAT-2022-16.pdf
- date added to LUP
- 2022-09-01 18:26:07
- date last changed
- 2023-11-19 18:06:25
@inproceedings{49687a3e-73d1-4fbd-ab14-09073b3d86ab,
abstract = {{The dramatic improvements in Boolean satisfiability (SAT) solving since the turn of the millennium have made it possible to leverage state-of-the-art conflict-driven clause learning (CDCL) solvers for many combinatorial problems in academia and industry, and the use of proof logging has played a crucial role in increasing the confidence that the results these solvers produce are correct. However, the fact that SAT proof logging is performed in conjunctive normal form (CNF) clausal format means that it has not been possible to extend guarantees of correctness to the use of SAT solvers for more expressive combinatorial paradigms, where the first step is an unverified translation of the input to CNF.<br/>In this work, we show how cutting-planes-based reasoning can provide proof logging for solvers that translate pseudo-Boolean (a.k.a. 0-1 integer linear) decision problems to CNF and then run CDCL. To support a wide range of encodings, we provide a uniform and easily extensible framework for proof logging of CNF translations. We are hopeful that this is just a first step towards providing a unified proof logging approach that will also extend to maximum satisfiability (MaxSAT) solving and pseudo-Boolean optimization in general.}},
author = {{Gocht, Stephan and Martins, Ruben and Nordström, Jakob and Oertel, Andy}},
booktitle = {{25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)}},
editor = {{Meel, Kuldeep S. and Strichman, Ofer}},
isbn = {{978-3-95977-242-6}},
issn = {{1868-8969}},
language = {{eng}},
month = {{07}},
publisher = {{Schloss Dagstuhl - Leibniz-Zentrum für Informatik}},
series = {{Leibniz International Proceedings in Informatics (LIPIcs)}},
title = {{Certified CNF Translations for Pseudo-Boolean Solving}},
url = {{http://dx.doi.org/10.4230/LIPIcs.SAT.2022.16}},
doi = {{10.4230/LIPIcs.SAT.2022.16}},
volume = {{236}},
year = {{2022}},
}