dc.contributor.author | Li, Zijie | |
dc.date.accessioned | 2009-10-08 18:24:57 (GMT) | |
dc.date.available | 2009-10-08 18:24:57 (GMT) | |
dc.date.issued | 2009-10-08T18:24:57Z | |
dc.date.submitted | 2009 | |
dc.identifier.uri | http://hdl.handle.net/10012/4810 | |
dc.description.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. | en |
dc.language.iso | en | en |
dc.publisher | University of Waterloo | en |
dc.subject | CSP | en |
dc.subject | SAT | en |
dc.subject | Backdoors | en |
dc.title | Backdoors in Satisfiability Problems | en |
dc.type | Master Thesis | en |
dc.pending | false | en |
dc.subject.program | Computer Science | en |
uws-etd.degree.department | School of Computer Science | en |
uws-etd.degree | Master of Mathematics | en |
uws.typeOfResource | Text | en |
uws.peerReviewStatus | Unreviewed | en |
uws.scholarLevel | Graduate | en |