Backdoors to acyclic SAT

DOI10.1007/978-3-642-31594-7_31MaRDI QIDQ2843262zbMATH OpenOpenAlexFDO

Authors Serge Gaspers, Stefan Szeider

Publication date 12 August 2013

Published in Automata, Languages, and Programming (Search for Journal in Brave)

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

Mathematics Subject Classification ID

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

Abstract: 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"os-P'osa Theorem, Courcelle's model checking for monadic second order logic, and new combinatorial results on how disjoint cycles can interact with the backdoor set.

Recommendations

• Backdoor treewidth for SAT
• Satisfiability of acyclic and almost acyclic CNF formulas
• Satisfiability of acyclic and almost acyclic CNF formulas
• Solving d-SAT via Backdoors to Small Treewidth
• Backdoors to satisfaction

Cited in

(17)

• Upper and lower bounds for weak backdoor set detection
• scientific article; zbMATH DE number 7724246 (Why is no real title available?)
• Complexity and approximability of parameterized MAX-CSPs
• Backdoors to planning
• Matched Formulas and Backdoor Sets
• Backdoors into heterogeneous classes of SAT and CSP
• Solving d-SAT via Backdoors to Small Treewidth
• Backdoors to satisfaction
• Backdoor sets for DLL subsolvers
• Matched formulas and backdoor sets
• Strong backdoors to nested satisfiability
• Backdoor treewidth for SAT
• Backdoors to tractable answer set programming
• Backdoors into two occurrences
• The good, the bad, and the odd: cycles in answer-set programs
• ALIAS: a modular tool for finding backdoors for SAT
• A New Bound for an NP-Hard Subclass of 3-SAT Using Backdoors

This page was built for publication: Backdoors to acyclic SAT

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