The Parameterized Complexity of Reasoning Problems Beyond NP

摘要: Today's propositional satisfiability (SAT) solvers are extremely powerful and can be used as an efficient back-end for solving NP-complete problems. However, many fundamental problems in knowledge representation reasoning located at the second level of Polynomial Hierarchy or even higher, hence polynomial-time transformations to SAT not possible, unless hierarchy collapses. Recent research shows that certain cases one break through these complexity barriers by fixed-parameter tractable (fpt) reductions which exploit structural aspects problem instances terms parameters. In this paper we develop a general theoretical framework supports classification parameterized on whether they admit such fpt-reduction not. This is based several new classes. As running example, use classify consistency disjunctive answer set programming, with respect various natural We underpin robustness our theory providing characterization classes weighted QBF satisfiability, alternating Turing machines, first-order model checking. addition, provide compendium complete classes, including related Knowledge Representation Reasoning, Logic, Combinatorics.