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.
Identifer | oai:union.ndltd.org:WATERLOO/oai:uwspace.uwaterloo.ca:10012/4810 |
Date | January 2009 |
Creators | Li, Zijie |
Source Sets | University of Waterloo Electronic Theses Repository |
Language | English |
Detected Language | English |
Type | Thesis or Dissertation |
Page generated in 0.0014 seconds