Talks and Poster Presentations (with Proceedings-Entry):
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.
English abstract:
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.
Related Projects:
Project Head Stefan Szeider:
The Parameterized Complexity of Reasoning Problems
Created from the Publication Database of the Vienna University of Technology.