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
Volume
Number
Pages	269-280
Publisher
Keywords
Link
Abstract	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.