UWSpace staff members will be away from May 5th to 9th, 2025. We will not be responding to emails during this time. If there are any urgent issues, please contact GSPA at gsrecord@uwaterloo.ca. If any login or authentication issues arise during this time, please wait until UWSpace Staff members return on May 12th for support.
 

Backdoors in Satisfiability Problems

Loading...
Thumbnail Image

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

LC Subject Headings

Citation