TY - GEN

T1 - Certified CNF Translations for Pseudo-Boolean Solving

AU - Gocht, Stephan

AU - Martins, Ruben

AU - Nordström, Jakob

AU - Oertel, Andy

N1 - Publisher Copyright: © Stephan Gocht, Ruben Martins, Jakob Nordström, and Andy Oertel.

PY - 2022

Y1 - 2022

N2 - 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.

AB - 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.

KW - 0-1 integer linear program

KW - certified translation

KW - certifying algorithms

KW - CNF encoding

KW - cutting planes

KW - proof logging

KW - pseudo-Boolean solving

U2 - 10.4230/LIPIcs.SAT.2022.16

DO - 10.4230/LIPIcs.SAT.2022.16

M3 - Article in proceedings

AN - SCOPUS:85136121900

T3 - Leibniz International Proceedings in Informatics, LIPIcs

BT - 25th International Conference on Theory and Applications of Satisfiability Testing, SAT 2022

A2 - Meel, Kuldeep S.

A2 - Strichman, Ofer

PB - Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing

T2 - 25th International Conference on Theory and Applications of Satisfiability Testing, SAT 2022

Y2 - 2 August 2022 through 5 August 2022

ER -