View article

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) NO (1)), but that the detection of a weak backdoor set is W [2]-hard, implying that this problem is not fixed-parameter tractable.