Backdoors to Acyclic SAT

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 tau to X that reduces F to a satisfiable formula F[tau] 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 tau to X, the reduced formula F[tau] 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 algorithmic 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.