KR Conference 2014 Conference Paper
- Ronald de Haan
- Stefan Szeider
Realistic problem instances are not random and often contain some kind of “hidden structure. ” Recent research succeeded to exploit such hidden structure to break the complexity barriers between levels of the PH, for problems that arise in disjunctive answer set programming (Fichte and Szeider, 2013) and abductive reasoning (Pfandler, Rümmele, and Szeider, 2013). The idea is to exploit problem structure in terms of a problem parameter, and to develop reductions to SAT that can be computed efficiently as long as the problem parameter is reasonably small. The theory of parameterized complexity (Downey and Fellows, 1999; Flum and Grohe, 2006; Niedermeier, 2006) provides exactly the right type of reduction suitable for this purpose, called fixed-parameter tractable reductions, or fpt-reductions for short. Now, for a suitable choice of the parameter, one can aim at developing fpt-reductions from the hard problem under consideration to SAT. Such positive results go significantly beyond the state-ofthe-art of current research in parameterized complexity. By shifting the scope from fixed-parameter tractability to fptreducibility (to SAT), parameters can be less restrictive and hence larger classes of inputs can be processed efficiently. Therefore, the potential for positive tractability results is greatly enlarged. In fact, there are some known reductions that, in retrospect, can be seen as fpt-reductions to SAT. A prominent example is Bounded Model Checking (Biere et al., 1999), which can be seen as an fpt-reduction from the model checking problem for linear temporal logic (LTL), which is PSPACE-complete, to SAT, where the parameter is an upper bound on the size of a counterexample. Bounded Model Checking is widely used for hardware and software verification at industrial scale (Biere, 2009). New Contributions The aim of this paper is to establish a general theoretical framework that supports the classification of hard problems on whether they admit an fpt-reduction to SAT or not. The main contribution is the development of a new hardness theory that can be used to provide evidence that certain problems do not admit an fpt-reduction to SAT, similar to NP-hardness which provides evidence against polynomial-time tractability (Garey and Johnson, 1979) and W[1]-hardness which provides evidence against fixed-parameter tractability (Downey and Fellows, 1999). At the center of our theory are two hierarchies of parameterized complexity classes: the ∗-k hierarchy and the k-∗ hierarchy. We define the complexity classes in terms of weighted variants of the quantified Boolean satisfiability problem with 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 and reasoning are located at the second level of the Polynomial Hierarchy or even higher, and hence 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 which exploit structural aspects of problem instances in terms of 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. We instantiate our theory by classifying the complexities of several case study problems, with respect to various natural parameters. These case studies include the consistency problem for disjunctive answer set programming and a robust version of constraint satisfaction.