Detecting Backdoor Sets with Respect to Horn and Binary Clauses
Seventh International Conference on Theory and Applications of Satisfiability Testing (SAT 2004), 10-13 May, 2004, Vancouver, BC, Canada
Download:  [paper ps] [paper pdf]
Abstract:We study the parameterized complexity of detecting backdoor sets for instances of the propositional satisfiability problem (SAT) with respect to the polynomially solvable classes HORN and 2-CNF. A backdoor set is a subset of variables; for a strong backdoor set, the simplified formulas resulting from any setting of these variables is in a polynomially solvable class, and for a weak backdoor set, there exists one setting which puts the satisfiable simplified formula in the class. We show that with respect to both HORN and 2-CNF classes, the detection of a strong backdoor set is fixed-parameter tractable (the existence of a set of size k for a formula of length N can be decided in time f(k)N^O(1), but that the detection of a weak backdoor set is W-hard, implying that this problem is not fixed-parameter tractable.