Workshop on Automated Reasoning
Bridging the Gap between Theory and Practice

 
 
 

ARW

Background

Call for Papers

Accepted Abstracts

Programme

Venue

Facilities

Accommodation

Travel

Registration

 

Automated Reasoning Workshop 2009
(21st-22nd April 2009, Department of Computer Science, University of Liverpool)

Invited Talk: Stefan Szeider

Heuristic methods work often quite well on real-world instances of computational reasoning problems, contrasting the theoretical intractability of the problems. For example, state-of-the art satisfiability solvers solve routinely real-world instances with hundreds of thousands of variables; however no algorithm is known to solve instances with n variables in time 2o(n) (and it is believed that such algorithm does not exist). This discrepancy between theoretical performance guarantees and empirically observed problem hardness causes a huge gap between theory and practise. It is a widely accepted view that the good practical performance of heuristic methods is due to a "hidden structure" present in real-world problem instances. However, classical complexity theory focuses on one dimension only, the input size, and does not provide a suitable framework for studying how a hidden structure influences the hardness of a reasoning problem.

In this talk I will advocate the framework of Parameterized Complexity for the theoretical study of computational reasoning problems. Parameterized complexity considers, in addition to the input size, a secondary measure, the parameter. The parameter can represent, among others, the degree of hidden structure present in a reasoning problem. This two-dimensional setting allows a more fine grained complexity analysis with the potential of being closer to problems as they appear in the real world, and thus to narrow the gap between theory and practise. The central notion of Parameterized Complexity is fixed-parameter tractability which refers to solvability in time f(k)nc, where n denotes the input size, f is some function (usually exponential) of the parameter k and c is a constant. The subject splits into two complementary questions, each has its own mathematical toolkit and methods: how to design and improve fixed-parameter algorithms, and how to gather evidence that a problem is not fixed-parameter tractable for a certain parameterization.

The reasoning problems considered in this talk will include problems that arise in satisfiability solving, model counting, quantified Boolean formula evaluation, nonmonotonic reasoning and constraint satisfaction. I will mainly focus on two groups of parameters: parameters that represent decomposability of problems, and parameters that represent the existence of reasoning shortcuts through the search space in terms of backdoors. Most topics of the talk are covered by recent surveys.

 
 
 

Maintained by Ullrich Hustadt, U.Hustadt@liverpool.ac.uk, last updated Saturday, 18-Apr-2009 12:08:00 BST.