Publication: Finding small backdoors in SAT instances

All || By Area || By Year

Title Finding small backdoors in SAT instances
Authors/Editors* Z. Li, P. van Beek
Where published* Proceedings of the 24th Canadian Conference on Artificial Intelligence
How published* Proceedings
Year* 2011
Pages 269-280
Although propositional satisfiability (SAT) is NP-complete, state-of-the-art SAT solvers are able to solve large, practical instances. The concept of backdoors has been introduced to capture structural properties of instances. A backdoor is a set of variables that, if assigned correctly, leads to a polynomial-time solvable sub-problem. In this paper, we address the problem of finding all small backdoors, which is essential for studying value and variable ordering mistakes. We discuss our definition of sub-solvers and propose algorithms for finding backdoors. We experimentally compare our proposed algorithms to previous algorithms on 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 8 of list