SAT 2004 START ConferenceManager    


Detecting Backdoor Sets with Respect to Horn and Binary Clauses

Naomi Nishimura, Prabhakar Ragde, and Stefan Szeider

Presented at The Seventh International Conference on Theory and Applications of Satisfiability Testing (SAT 2004), Vancouver, BC, Canada, 10-13 May 2004


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. The notion of backdoor sets was recently introduced by Williams, Gomes, and Selman.

We show that with respect to both HORN and 2-CNF, the detection of a strong backdoor set is fixed-parameter tractable (i.e., 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.


  
START Conference Manager (V2.47.2)
Maintainer: rrgerber@softconf.com