"Advanced Redundancy-Based Methods for SAT"
, Linz, 8-2022
Advanced Redundancy-Based Methods for SAT
Sprache des Titels:
The Boolean satisfiability (SAT) problem, deciding whether a formula in Boolean logic has a satisfying assignment, has become a fundamental problem in computer science and automated reasoning. Despite the absence of any known polynomial-time algorithm, SAT solving tools have become highly effective in practice, capable of handling large-scale instances from industrial applications. While the success of modern SAT solvers can be attributed to several factors, notable recent progress has been made by exploring the use of redundant clauses: disjunctions of literals that can be added to, or removed from, a formula while preserving satisfiability, though not necessarily logical equivalence. Current techniques utilizing redundant clauses, such as powerful proof systems and clause elimination procedures, show the potential of redundancy-based methods for SAT solving, but are not easily compatible with important solving procedures. This thesis explores limitations of current redundancy-based methods and presents novel approaches to redundancy-based reasoning in SAT.
We examine an important class of redundant clauses called covered clauses, which generalize multiple redundancy properties used by SAT solvers for clause elimination. Such formula simplification methods are demonstrably beneficial for solving large SAT instances from various application areas, though they may alter a formula?s solution set, requiring a separate solution reconstruction process. Procedures based on covered clauses use a reconstruction process that is more complex and burdensome than similar procedures. We prove that for covered clauses, the partial assignments known as witnesses used by the typical solution reconstruction process can be as difficult to produce as solving the formula itself. We also show that covered clauses are not captured by the property used by the powerful propagation redundancy (PR) proof system. Furthermore, we develop a more flexible and general structure for witnesses to allow for efficient solution reconstruction for covered clauses as well.
This thesis also develops methods for reasoning about redundant but non-clausal Boolean constraints. Strong proof systems for certifying SAT solvers? results, and increasing trust in SAT technology, are based on the iterative addition of redundant clauses to a formula, but can struggle to express solving techniques that are not naturally in clause form. In particular, reasoning over "exclusive-or" (XOR) constraints embedded in a formula can afford tremendous gains in efficiency, but complicates the production of proofs, typically causing solvers to disable XOR reasoning when proofs are required. We generalize the notion of redundancy for clauses to redundancy for Boolean functions, retaining the strengths of clausal proof systems while expressing non-clausal reasoning. We use binary decision diagrams to represent redundant Boolean functions, producing proofs that capture XOR reasoning in a natural way. To show the effectiveness of this approach in practice, we present the results of a preliminary implementation of a proof checking tool which uses this method.