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. © 2012 Springer-Verlag.
CITATION STYLE
Gaspers, S., & Szeider, S. (2012). Strong backdoors to nested satisfiability. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7317 LNCS, pp. 72–85). https://doi.org/10.1007/978-3-642-31612-8_7
Mendeley helps you to discover research relevant for your work.