We use cookies to ensure that we give you the best experience on our website. By continuing to browse this repository, you give consent for essential cookies to be used. You can read more about our Privacy and Cookie Policy.

Durham Research Online
You are in:

Backdoor sets for DLL subsolvers.

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.

Item Type:Article
Keywords:satisfiability - unit propagation - pure literal elimination - backdoor sets - parameterized complexity - W[P]-completeness.
Full text:(AM) Accepted Manuscript
Download PDF
Publisher Web site:
Publisher statement:The original publication is available at
Record Created:14 Oct 2008
Last Modified:10 Aug 2011 16:33

Social bookmarking: del.icio.usConnoteaBibSonomyCiteULikeFacebookTwitterExport: EndNote, Zotero | BibTex
Look up in GoogleScholar | Find in a UK Library