| الوصف: |
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. |
