[Back]

S. Gaspers, St. Szeider:
"Backdoors to Acyclic SAT";
Talk: International Colloquium on Automata, Languages and Programming (ICALP), Warwick, UK; 2012-07-09 - 2012-07-13; in: "Proceedings of the 39th International Colloquium on Automata, Languages and Programming (ICALP 2012)", Springer-Verlag, Lecture Notes in Computer Science / Vol. 7391 (2012), ISBN: 978-3-642-31593-0; 363 - 374.

Backdoor sets contain certain key variables of a CNF formula F that make it easy to solve the formula. More specifically, a weak backdoor set of F is a set X of variables such that there exits a truth assignment τ to X that reduces F to a satisfiable formula F[τ] that belongs to a polynomial-time decidable base class C. A strong backdoor set is a set X of variables such that for all assignments τ to X, the reduced formula F[τ] belongs to C.
We study the problem of finding backdoor sets of size at most k with respect to the base class of CNF formulas with acyclic incidence graphs, taking k as the parameter. We show that
1. the detection of weak backdoor sets is W[2]-hard in general but fixed-parameter tractable for r-CNF formulas, for any fixed r ≥ 3, and 2. the detection of strong backdoor sets is fixed-parameter approximable. Result 1 is the the first positive one for a base class that does not have a characterization with obstructions of bounded size. Result 2 is the first positive one for a base class for which strong backdoor sets are more powerful than deletion backdoor sets.
Not only SAT, but also #SAT can be solved in polynomial time for CNF formulas with acyclic incidence graphs. Hence Result 2 establishes a new structural parameter that makes #SAT fixed-parameter tractable and that is incomparable with known parameters such as treewidth and clique-width. We obtain the algorithms by a combination of an algo- rithmic version of the Erdos-Posa Theorem, Courcelle´s model checking for monadic second order logic, and new combinatorial results on how disjoint cycles can interact with the backdoor set.

http://dx.doi.org/10.1007/978-3-642-31594-7_31

Project Head Stefan Szeider:
The Parameterized Complexity of Reasoning Problems