Strong Backdoors to Nested Satisfiability

TL;DR

This paper presents a fixed-parameter tractable algorithm for satisfiability of CNF formulas parameterized by the size of a strong backdoor set to nested formulas, using graph minor theory and combinatorial techniques.

Contribution

It introduces a novel FPT algorithm leveraging graph minors and backdoor sets to efficiently decide satisfiability for formulas close to nested formulas.

Findings

Algorithm finds small backdoor sets efficiently.

Decides satisfiability in polynomial time with bounded backdoor size.

Uses graph minor theory to analyze formula structure.

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 target class of nested formulas, checking the satisfiability 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 variable set B of size at most k such that for every truth assignment t to B, the formula F[t] 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 using 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 is decided.