  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.
