Title: Interference-based proofs in SAT solving
Language: English
Authors: Rebola Pardo, Adrian 
Qualification level: Doctoral
Advisor: Weissenbacher, Georg 
Issue Date: 2022
Rebola Pardo, A. (2022). Interference-based proofs in SAT solving [Dissertation, Technische Universität Wien]. reposiTUm. https://doi.org/10.34726/hss.2022.102507
Number of Pages: 186
Qualification level: Doctoral
One of the main advancements in SAT solving over the last decade was the development of a family of proof systems collectively called interference-based proof systems, including but not limited to DRAT. These proof systems aim at easily expressing inprocessing techniques, modes of reasoning that are complex or impossible to express within resolution. As expressive as they are, these proof systems are notoriously complicated to work with. Interference reasoning rules are global and depend on the whole formula the solver is processing. In particular, some rules depend not only on the presence of some clauses, but also on their absence. This has widespread implications, from the loss of model preservation, replaced by the much weaker invariant of satisfiability preservation; to the linear structure of proofs, as opposed to the more traditional tree structure. Furthermore, the interference framework takes clause deletions into account, which now have semantic content; some issues with the applicability of deletions appeared as well, creating a division between operational proof checking and specified proof checking. In this dissertation, we explore several issues concerning interference-based proofs. We elucidate the compared properties of specified and operational proof checking, developing the first specified DRAT checker with competitive performance. Furthermore, we examine the structural and semantic properties of interference-based proofs. We develop an algorithm that transforms DRAT proofs into a resolution-like proof system; this enables the generation of interpolants from a DRAT proof. Finally, a new perspective over interference-based proofs is introduced by translating proofs into a richer logic. In particular, in this framework interference can be understood as reasoning without loss of generality. Under this perspective, the usual properties of traditional proof systems, such as tree-like dependencies and model preservation, are recovered. In addition, this new perspective immediately pointed towards possible generalizations of interference- based proof systems. We propose the novel WSR proof system and show improvements in usability and proof length.
Keywords: SAT solving; Proof systems; Interference; Interpolation
URI: https://doi.org/10.34726/hss.2022.102507
DOI: 10.34726/hss.2022.102507
Library ID: AC16522179
Organisation: E192 - Institut für Logic and Computation 
Publication Type: Thesis
Appears in Collections:Thesis

Files in this item:

Items in reposiTUm are protected by copyright, with all rights reserved, unless otherwise indicated.

Page view(s)

checked on May 20, 2022


checked on May 20, 2022

Google ScholarTM