Detecting Backdoor Sets with Respect to Horn and Binary ClausesSeventh 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[2]-hard, implying that this problem is not fixed-parameter tractable.[back to Stefan Szeider's homepage] |