A Theory of Satisability-Preserving Proofs in SAT Solving
The result's identifiers
Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F68407700%3A21730%2F18%3A00329606" target="_blank" >RIV/68407700:21730/18:00329606 - isvavai.cz</a>
Result on the web
<a href="https://easychair.org/publications/paper/zr7z" target="_blank" >https://easychair.org/publications/paper/zr7z</a>
DOI - Digital Object Identifier
<a href="http://dx.doi.org/10.29007/tc7q" target="_blank" >10.29007/tc7q</a>
Alternative languages
Result language
angličtina
Original language name
A Theory of Satisability-Preserving Proofs in SAT Solving
Original language description
We study the semantics of propositional interference-based proof systems such as DRAT and DPR. These are characterized by modifying a CNF formula in ways that preserve satis_ability but not necessarily logical truth. We propose an extension of propositional logic called overwrite logic with a new construct which captures the meta-level reasoning behind interferences. We analyze this new logic from the point of view of expressivity and complexity, showing that while greater expressivity is achieved, the satis_ability problém for overwrite logic is essentially as hard as SAT, and can be reduced in a way that is well-behaved for modern SAT solvers. We also show that DRAT and DPR proofs can be seen as overwrite logic proofs which preserve logical truth. This much stronger invariant than the mere satis_ability preservation maintained by the traditional view gives us better understanding on these practically important proof systems. Finally, we showcase this better understanding by _nding intrinsic limitations in interference-based proof systems.
Czech name
—
Czech description
—
Classification
Type
J<sub>ost</sub> - Miscellaneous article in a specialist periodical
CEP classification
—
OECD FORD branch
10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)
Result continuities
Project
—
Continuities
R - Projekt Ramcoveho programu EK
Others
Publication year
2018
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Data specific for result type
Name of the periodical
EPiC Series in Computing
ISSN
2398-7340
e-ISSN
2398-7340
Volume of the periodical
8
Issue of the periodical within the volume
57
Country of publishing house
GB - UNITED KINGDOM
Number of pages
21
Pages from-to
583-603
UT code for WoS article
—
EID of the result in the Scopus database
—