A Theory of Satisability-Preserving Proofs in SAT Solving

Kód výsledku v 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>

Výsledek na webu

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

Jazyk výsledku

angličtina

Název v původním jazyce

A Theory of Satisability-Preserving Proofs in SAT Solving

Popis výsledku v původním jazyce

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.

Název v anglickém jazyce

A Theory of Satisability-Preserving Proofs in SAT Solving

Popis výsledku anglicky

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.

Druh

J_ost - Ostatní články v recenzovaných periodicích

CEP obor

—

OECD FORD obor

10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

Projekt

—

Návaznosti

R - Projekt Ramcoveho programu EK

Rok uplatnění

2018

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Název periodika

EPiC Series in Computing

ISSN

2398-7340

e-ISSN

2398-7340

Svazek periodika

8

Číslo periodika v rámci svazku

57

Stát vydavatele periodika

GB - Spojené království Velké Británie a Severního Irska

Počet stran výsledku

21

Strana od-do

583-603

Kód UT WoS článku

—

EID výsledku v databázi Scopus

—