Szeider, S. (2005) 'Backdoor sets for DLL subsolvers.', Journal of automated reasoning., 35 (1-3). pp. 73-88.
We study the parameterized complexity of detecting small backdoor sets for instances of the propositional satisfiability problem (SAT). The notion of backdoor sets has been recently introduced by Williams, Gomes, and Selman for explaining the ‘heavy-tailed’ behavior of backtracking algorithms. If a small backdoor set is found, then the instance can be solved efficiently by the propagation and simplification mechanisms of a SAT solver. Empirical studies indicate that structured SAT instances coming from practical applications have small backdoor sets. We study the worst-case complexity of detecting backdoor sets with respect to the simplification and propagation mechanisms of the classic Davis–Logemann–Loveland (DLL) procedure. We show that the detection of backdoor sets of size bounded by a fixed integer k is of high parameterized complexity. In particular, we determine that this detection problem (and some of its variants) is complete for the parameterized complexity class W[P]. We achieve this result by means of a generalization of a reduction due to Abrahamson, Downey, and Fellows.
|Keywords:||satisfiability - unit propagation - pure literal elimination - backdoor sets - parameterized complexity - W[P]-completeness.|
|Full text:||PDF - Accepted Version (148Kb)|
|Publisher Web site:||http://dx.doi.org/doi:10.1007/s10817-005-9007-9|
|Publisher statement:||The original publication is available at www.springerlink.com|
|Record Created:||14 Oct 2008|
|Last Modified:||10 Aug 2011 16:33|
|Social bookmarking:||Export: EndNote, Zotero | BibTex|
|Usage statistics||Look up in GoogleScholar | Find in a UK Library|