Backdoors to Acyclic SAT

Serge Gaspers and Stefan Szeider

Proceedings of ICALP 2012 (Track A: Algorithms, Complexity and Games), the 39th International Colloquium on Automata, Languages and Programming, 9-13 July 2012, University of Warwick, UK. Lecture Notes in Computer Science, vol. 7391, pp. 363-374, Springer-Verlag, 2012.

Abstract:

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

Preprint available from Arxiv.org: 1110.6384.