Parameterized complexity classes beyond para-NP

- We develop parameterized complexity classes that can be used to provide evidence that problems are not fpt-reducible to SAT.
- We show that these classes can be characterized by means of several fundamental concepts from theoretical computer science.
- We show how these classes can be employed in the computational complexity analysis of many natural parameterized problems.
- We give evidence that these classes are different from parameterized complexity classes that are known from the literature.
- We provide a compendium of natural parameterized problems that are complete for the new parameterized complexity classes.

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 logic, in knowledge representation and reasoning, and in artificial intelligence are located at the second level of the Polynomial Hierarchy or even higher, and hence for these problems polynomial-time transformations to SAT are not possible, unless the hierarchy collapses. Recent research shows that in certain cases one can break through these complexity barriers by fixed-parameter tractable (fpt) reductions to SAT which exploit structural aspects of problem instances in terms of problem parameters. These reductions are more powerful because their running times can grow superpolynomially in the problem parameters. In this paper we develop a general theoretical framework that supports the classification of parameterized problems on whether they admit such an fpt-reduction to SAT or not.