Backdoor Sets for DLL Subsolvers

Szeider, Stefan

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.
• Public URL: https://durham-repository.worktribe.com/output/1597182