Computer Science – Data Structures and Algorithms
Scientific paper
2012-02-20
Computer Science
Data Structures and Algorithms
Scientific paper
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.
Gaspers Serge
Szeider Stefan
No associations
LandOfFree
Strong Backdoors to Nested Satisfiability does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.
If you have personal experience with Strong Backdoors to Nested Satisfiability, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Strong Backdoors to Nested Satisfiability will most certainly appreciate the feedback.
Profile ID: LFWR-SCP-O-564871