Publication: Backdoors in Satisfiability Problems

All || By Area || By Year

Title Backdoors in Satisfiability Problems
Authors/Editors* Zijie Li
Where published* MMath thesis, University of Waterloo
How published* Thesis
Year* 2009
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.
Go to Artificial intelligence
Back to page 36 of list