Skip to main content

Research Repository

Advanced Search

Backdoor Sets for DLL Subsolvers

Szeider, Stefan

Backdoor Sets for DLL Subsolvers Thumbnail


Authors

Stefan Szeider



Abstract

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.

Citation

Szeider, S. (2005). Backdoor Sets for DLL Subsolvers. Journal of Automated Reasoning, 35(1-3), 73-88. https://doi.org/10.1007/s10817-005-9007-9

Journal Article Type Article
Publication Date 2005-10
Deposit Date Oct 14, 2008
Publicly Available Date Oct 14, 2008
Journal Journal of Automated Reasoning
Print ISSN 0168-7433
Electronic ISSN 1573-0670
Publisher Springer
Peer Reviewed Peer Reviewed
Volume 35
Issue 1-3
Pages 73-88
DOI https://doi.org/10.1007/s10817-005-9007-9
Keywords satisfiability - unit propagation - pure literal elimination - backdoor sets - parameterized complexity - W[P]-completeness.

Files

Accepted Journal Article (151 Kb)
PDF

Copyright Statement
The original publication is available at www.springerlink.com





You might also like



Downloadable Citations