[Back]

S. Gaspers, St. Szeider:
"Strong Backdoors to Nested Satisfiability";
Talk: International Conference on Theory and Applications of Satisfiability Testing (SAT), Trento, Italy; 2012-06-17 - 2012-06-20; in: "Proceedings of the Fifteen International Conference on Theory and Applications of Satisfiability Testing (SAT 2012)", A. Cimatti, R. Sebastiani (ed.); LNCS / Springer, 7317 (2012), ISBN: 978-3-642-31611-1; 58 - 71.

Knuth (1990) introduced the class of nested formulas and showed that their satisfiability can be decided in polynomial time. We show that, parameterized by the size of a smallest strong backdoor set to the base class of nested formulas, computing the number of satisfying assignments of any CNF formula is fixed-parameter tractable. Thus, for any k > 0, the satisfiability problem can be solved in polynomial time for any formula F for which there exists a set B of at most k variables such that for every truth assignment τ to B, the reduced formula F[τ] is nested; moreover, the degree of the polynomial is independent of k.
Our algorithm uses the grid-minor theorem of Robertson and Seymour (1986) to either find that the incidence graph of the formula has bounded treewidth-a case that is solved by model checking for monadic second order logic-or to find many vertex-disjoint obstructions in the incidence graph. For the latter case, new combinatorial arguments are used to find a small backdoor set. Combining both cases leads to an approximation algorithm producing a strong backdoor set whose size is upper bounded by a function of the optimum. Going through all assignments to this set of variables and using Knuth´s algorithm, the satisfiability of the input formula can be decided. With a similar approach, one can also count the number of satisfying assignments of the given formula.

Project Head Stefan Szeider:
The Parameterized Complexity of Reasoning Problems