Backdoors in Satisfiability Problems
Loading...
Date
2009-10-08T18:24:57Z
Authors
Li, Zijie
Advisor
Journal Title
Journal ISSN
Volume Title
Publisher
University of Waterloo
Abstract
Although satisfiability problems (SAT) are NP-complete, state-of-the-art SAT solvers are able to solve large practical instances. The notion of backdoors has been introduced to capture structural properties of instances. Backdoors are a set of variables for which there exists some value assignment that leads to a polynomial-time solvable sub-problem. I address in this thesis the problem of finding all minimal backdoors, which is essential for studying value and variable ordering mistakes. I discuss our definition of sub-solvers and propose algorithms for finding backdoors. I implement our proposed algorithms by modifying a state-of-the-art SAT solver, Minisat. I analyze experimental results comparing our proposed algorithms to previous algorithms applied to random 3SAT, structured, and real-world instances. Our proposed algorithms improve over previous algorithms for finding backdoors in two ways. First, our algorithms often find smaller backdoors. Second, our algorithms often find a much larger number of backdoors.
Description
Keywords
CSP, SAT, Backdoors