Backdoors to normality for disjunctive logic programs
From MaRDI portal
Abstract: Over the last two decades, propositional satisfiability (SAT) has become one of the most successful and widely applied techniques for the solution of NP-complete problems. The aim of this paper is to investigate theoretically how Sat can be utilized for the efficient solution of problems that are harder than NP or co-NP. In particular, we consider the fundamental reasoning problems in propositional disjunctive answer set programming (ASP), Brave Reasoning and Skeptical Reasoning, which ask whether a given atom is contained in at least one or in all answer sets, respectively. Both problems are located at the second level of the Polynomial Hierarchy and thus assumed to be harder than NP or co-NP. One cannot transform these two reasoning problems into SAT in polynomial time, unless the Polynomial Hierarchy collapses. We show that certain structural aspects of disjunctive logic programs can be utilized to break through this complexity barrier, using new techniques from Parameterized Complexity. In particular, we exhibit transformations from Brave and Skeptical Reasoning to SAT that run in time O(2^k n^2) where k is a structural parameter of the instance and n the input size. In other words, the reduction is fixed-parameter tractable for parameter k. As the parameter k we take the size of a smallest backdoor with respect to the class of normal (i.e., disjunction-free) programs. Such a backdoor is a set of atoms that when deleted makes the program normal. In consequence, the combinatorial explosion, which is expected when transforming a problem from the second level of the Polynomial Hierarchy to the first level, can now be confined to the parameter k, while the running time of the reduction is polynomial in the input size n, where the order of the polynomial is independent of k.
Recommendations
Cites work
- Answer set programming based on propositional satisfiability
- ASSAT: computing answer sets of a logic program by SAT solvers
- Backdoors to satisfaction
- Backdoors to tractable answer set programming
- Characterizations of the disjunctive well-founded semantics: Confluent calculi and iterated GCWA
- Computing Stable Models via Reductions to Difference Logic
- Conflict-driven answer set solving: from theory to practice
- Describing parameterized complexity classes
- Detecting inconsistencies in large biological networks with answer set programming
- Empirical study of the anatomy of modern SAT solvers
- Extending and implementing the stable model semantics
- Fixed-parameter tractable reductions to SAT
- Fundamentals of parameterized complexity
- scientific article; zbMATH DE number 5914356 (Why is no real title available?)
- scientific article; zbMATH DE number 25190 (Why is no real title available?)
- scientific article; zbMATH DE number 1324669 (Why is no real title available?)
- scientific article; zbMATH DE number 610968 (Why is no real title available?)
- scientific article; zbMATH DE number 1979551 (Why is no real title available?)
- scientific article; zbMATH DE number 1507224 (Why is no real title available?)
- scientific article; zbMATH DE number 6747915 (Why is no real title available?)
- scientific article; zbMATH DE number 5493266 (Why is no real title available?)
- scientific article; zbMATH DE number 2234775 (Why is no real title available?)
- Improved Parameterized Upper Bounds for Vertex Cover
- Integrating dependency schemes in search-based QBF solvers
- Linear-time algorithms for testing the satisfiability of propositional horn formulae
- Logic Programming and Nonmonotonic Reasoning
- Logic programs with stable model semantics as a constraint programming paradigm
- Long-distance resolution: proof generation and strategy extraction in search-based QBF solving
- Modularity aspects of disjunctive stable models
- Negation by default and unstratifiable logic programs
- On the computational cost of disjunctive logic programming: Propositional case
- Propositional semantics for disjunctive logic programs
- Some (in)translatability results for normal logic programs and propositional theories
- The DLV system for knowledge representation and reasoning
- The Semantics of Predicate Logic as a Programming Language
- Theory and Applications of Satisfiability Testing
- Theory and Applications of Satisfiability Testing
- Trichotomy and dichotomy results on the complexity of reasoning with disjunctive logic programs
- Unfolding partiality and disjunctions in stable model semantics
- Why are there so many loop formulas?
Cited in
(13)- A multiparametric view on answer set programming
- Backdoors to planning
- Backdoors to tractable answer set programming
- Strong Backdoors for Default Logic
- Trichotomy Results on the Complexity of Reasoning with Disjunctive Logic Programs
- Tradeoffs in the complexity of backdoors to satisfiability: dynamic sub-solvers and learning during search
- Dual-normal logic programs -- the forgotten class
- Backdoor sets for CSP
- The good, the bad, and the odd: cycles in answer-set programs
- Parameterised complexity of model checking and satisfiability in propositional dependence logic
- Backdoor DNFs
- Strong backdoors for default logic
- Strong backdoors for default logic
This page was built for publication: Backdoors to normality for disjunctive logic programs
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5277908)