Backdoors to Normality for Disjunctive Logic Programs

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 Cautious 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. We cannot transform these two reasoning problems to SAT in polynomial time, unless the Polynomial Hierarchy collapses. We show that certain structural aspects of logic programs can be utilized to break through this complexity barrier, using new techniques from Parameterized Complexity. Such a backdoor is a set of atoms that when deleted makes the program normal. We show that such a transformation is not possible if we consider backdoors with respect to tightness instead of normality.