2011/10/28 by Serge Gaspers, Stefan Szeider, Gaspers, Serge +1 · 2 citations
Computer Science · Mathematics · #Algorithms and Data Compression #Artificial Intelligence (cs.AI) #Combinatorics (math.CO) #Computational Complexity (cs.CC) #Data Structures and Algorithms (cs.DS) #FOS: Computer and information sciences #FOS: Mathematics #Formal Methods in Verification #Software Testing and Debugging Techniques #cs.AI #cs.CC #cs.DS #math.CO
paper · pdf · doi:10.48550/arxiv.1110.6384
openalex publication_date 2011/10/28 · arxiv created 2012/02/21 · arxiv updated 2012/02/22 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
Backdoor sets, a notion introduced by Williams et al. in 2003, are certain sets of key variables of a CNF formula F that make it easy to solve the formula; by assigning truth values to the variables in a backdoor set, the formula gets reduced to one or several polynomial-time solvable formulas. More specifically, a weak backdoor set of F is a set X of variables such that there exits a truth assignment t to X that reduces F to a satisfiable formula F[t] that belongs to a polynomial-time decidable base class C. A strong backdoor set is a set X of variables such that for all assignments t to X, the reduced formula F[t] belongs to C. We study the problem of finding backdoor sets of size at most k with respect to the base class of CNF formulas with acyclic incidence graphs, taking k as the parameter. We show that 1. the detection of weak backdoor sets is W[2]-hard in general but fixed-parameter tractable for r-CNF formulas, for any fixed r>=3, and 2. the detection of strong backdoor sets is fixed-parameter approximable. Result 1 is the the first positive one for a base class that does not have a characterization with obstructions of bounded size. Result 2 is the first positive one for a base class for which strong backdoor sets are more powerful than deletion backdoor sets. Not only SAT, but also #SAT can be solved in polynomial time for CNF formulas with acyclic incidence graphs. Hence Result 2 establishes a new structural parameter that makes #SAT fixed-parameter tractable and that is incomparable with known parameters such as treewidth and clique-width. We obtain the algorithms by a combination of an algorithmic version of the Erdös-Pósa Theorem, Courcelle's model checking for monadic second order logic, and new combinatorial results on how disjoint cycles can interact with the backdoor set.