Solving d-SAT via backdoors to small treewidth

The VCLA and WPI will host a talk by M. S. Ramanujan on September 30, 2014.

ABSTRACT

A backdoor set of a CNF formula is a set of variables such that fixing the truth values of the variables from this set moves the formula into a polynomial-time decidable class. In this work we obtain several algorithmic results for solving d-SAT, by exploiting backdoors to d-CNF formulas whose incidence graphs have small treewidth.   For a CNF formula $phi$ and integer t, a strong backdoor set to treewidth t is a set of variables such that each possible partial assignment to this set reduces $phi$ to a formula whose incidence graph is of treewidth at most t. A weak backdoor set to treewidth t is a set of variables such that there is a partial assignment to this set that reduces $phi$ to a satisfiable formula of treewidth at most t. Our main contribution is an algorithm that, given a $d$-CNF formula $phi$ and an integer k, in time $2^{O(k)} | phi |$,   1. either finds a satisfying assignment of $phi$, or   2. reports correctly that $phi$ is not satisfiable, or   3. concludes correctly that $phi$ has neither a weak nor a strong backdoor set to treewidth t of size at most k.   As a consequence of the above, we show that $d$-SAT parameterized by the size of a smallest weak/strong backdoor set to formulas of treewidth $t$, is fixed-parameter tractable. Prior to our work, such results were know only for the special case of t=1 (Gaspers and Szeider, ICALP 2012).   Along the way, we introduce a linear time "protrusion replacer" improving over a $O(nlog^2{n})$-time procedure of Fomin et al. (FOCS 2012). The new deterministic linear time protrusion replacer has several applications in kernelization and parameterized algorithms.