Backdoor Sets for DLL Subsolvers
Backdoor Sets for DLL Subsolvers
复制标题
DOI：
10.1007/s10817-005-9007-9
复制
发表时间：
2005-10
期刊：
影响因子：
--
通讯作者：
Stefan Szeider
中科院分区：
文献类型：
--
作者：
Stefan Szeider
研究了命题可满足性问题（SAT）小后门集检测的参数化复杂性.后门集的概念最近由威廉姆斯、戈麦斯和塞尔曼引入，用于解释回溯算法的“重尾”行为。如果找到一个小的后门集，则可以通过SAT求解器的传播和简化机制有效地求解该实例。实证研究表明，来自实际应用的结构化SAT实例具有较小的后门集。我们研究了经典的Davis-Logemann-洛夫兰（DLL）过程的简化和传播机制检测后门集的最坏情况的复杂度。我们发现，检测后门集的大小由一个固定的integerkis高参数化的复杂性。特别地，我们确定这个检测问题（及其一些变体）对于参数化复杂性类W[P]是完全的。我们通过推广Abrahamson、唐尼和Fellows的约化得到了这个结果。
We study the parameterized complexity of detecting smallbackdoor setsfor 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 integerkis 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.