Strong backdoors to nested satisfiability

DOI10.1007/978-3-642-31612-8_7MaRDI QIDQ2843323zbMATH OpenOpenAlexFDO

Authors Serge Gaspers, Stefan Szeider

Publication date 12 August 2013

Published in Theory and Applications of Satisfiability Testing – SAT 2012 (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1202.4331

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)

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.

Recommendations

• Backdoors to acyclic SAT
• Backdoor treewidth for SAT
• Solving d-SAT via Backdoors to Small Treewidth
• Backdoors to satisfaction
• Solving \#SAT using vertex covers

Cited in

(9)

• Satisfiability of co-nested formulas
• Backdoor treewidth for SAT
• Backdoors to tractable answer set programming
• Strong Backdoors for Default Logic
• Backdoors to satisfaction
• Solving d-SAT via Backdoors to Small Treewidth
• scientific article; zbMATH DE number 7724246 (Why is no real title available?)
• Optimization and probabilistic satisfiability on nested and co-nested formulas
• Backdoors into heterogeneous classes of SAT and CSP

This page was built for publication: Strong backdoors to nested satisfiability

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2843323)