E192-03 - Forschungsbereich Knowledge Based Systems
Automata, Languages, and Programming
International Colloquium on Automata, Languages and Programming (ICALP)
9-Jul-2012 - 13-Jul-2012
Warwick, UK, EU
Number of Pages:
Springer-Verlag, Lecture Notes in Computer Science / Vol. 7391
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-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.
The Parameterized Complexity of Reasoning Problems: 239962 (Europäischer Forschungsrat (ERC))