Ronald de Haan,

TU Wien –

Abstract:

Modern propositional satisfiability (SAT) solvers perform extremely well in many practical settings 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 (PH) or even higher, and hence for these problems polynomial-time transformations to SAT are not possible, unless the PH 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.
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 base this framework on its application to concrete reasoning problems from various domains. We develop several parameterized complexity classes to provide evidence that in certain cases such fpt-reductions to SAT are not possible. Moreover, we relate these new classes to existing parameterized complexity classes. Additionally, for problems for which there exists a Turing fpt-reduction to SAT, we develop techniques to provide lower bounds on the number of calls to a SAT solver needed to solve these problems.

 

Date: 2014-Apr-02     Time: 14:00:00     Room: 336

For more information: