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.

研究了如何利用命题可满足性 (SAT) 解决比 NP 或 co-NP 更困难的问题，特别是对命题析取答案集编程中的基本推理问题进行探讨，介绍了利用新的 Parameterized Complexity 技术从 Brave 和 Skeptical Reasoning 转换到 SAT 的方法。

非连续逻辑程序的回归正常