Parameterized Complexity of Computational Reasoning

Satellite Workshop of MFCS & CSL 2010, Brno, Czech Republic, 28 August 2010

Aims & Scope | Invited Speakers | Registration and Local Information | Schedule | Abstracts of Talks + Slides | Photos

Topics of interest include but are not limited to: multivariate analysis of reasoning problems, kernelization and preprocessing, fixed-parameter tractability and hardness, backdoors and decompositions.

The workshop will feature an invited keynote talk as well as several invited and contributed talks with surveys and new technical results. Apart from talks on parameterized complexity we are also interested in presentations that highlight structural parameters that have not been studied within the framework of parameterized complexity so far.

The workshop is organized by Igor Razgon, Marko Samer, Stefan Szeider (chair), and Stefan Woltran.

- Mike Fellows (keynote speaker), Charles Darwin University
- Nicola Galesi, Sapienza University of Rome
- Gregory Gutin, University of London
- Petr Hlineny, Masaryk University Brno
- Reinhard Pichler, Vienna University of Technology

To register online and for travel and accommodation information please consult the MFCS & CSL 2010 web pages.

Please note that you can register for the workshop alone without registering for the MFCS or CSL conferences. The early payment deadline for workshops is July 30, 2010.

8:30 | Welcome | |||

8:45 | — | 9:30 | Gregory GutinComplexity of Permutation Constraint Satisfaction Problems Parameterized Above Average
| |

9:30 | — | 10:00 | Coffee | |

10:00 | — | 11:00 | Mike
Fellows, Keynote Talk An Overview of Parameterized Complexity and Recent Research
Directions in Constraint Satisfaction and Artificial Intelligence | |

11:00 | — | 11:30 | Fran
RosamondOn the Complexity of Some Constraint Satisfaction Problems with Global Constraints and Convexity | |

11:30 | — | 12:15 | Reinhard
PichlerBounded Treewidth in Non-Monotonic Reasoning
| |

12:15 | — | 14:00 | Joint Lunch | |

14:00 | — | 14:45 | Petr
HlinenyWhere Myhill-Nerode Theorem Meets Parameterized Algorithmics | |

14:45 | — | 15:15 | M. PraveenDoes Treewidth Help in Modal Satisfiability? | |

15:15 | — | 15:45 | Coffee | |

15:45 | — | 16:30 | Nicola
GalesiThe Complexity of Proofs in Parameterized Resolution | |

16:30 | — | 17:00 | Yijia
ChenOptimal Proof systems, Slicewise
Monotone Parameterized Problems, and Logics for PTIME | |

17:00 | — | 17:15 | Break | |

17:15 | — | 17:45 | Open Problems, Discussion |

In this talk, I will explain the equivalence among three questions.

1. Does TAUT have a p-optimal proof system?

2. Is a specific natural parameterized halting problem in uniform XP?

3. Does a logic introduced by Blass and Gurevich capture PTIME?

Moreover, I will discuss some generalization of the problems.

This is joint work with Jörg Flum.

The talk will survey the basic ideas of parameterized complexity and recent developments in the field, with attention to applications in constraint satisfaction and artificial intelligence.

Parameterized Proof Complexity was introduced by Dantchev, Martin, and
Szeider in 2007. In the talk we consider the system of Parameterized Resolution and we
focus and broadly analyze the complexity of proofs in this system.

First we introduce a purely combinatorial approach to obtain lower bounds to
the proof size
in tree-like Parameterized Resolution based on a new asymmetric Prover-Delayer game which characterizes proofs in tree-like Resolution.

Second, interpreting a well-known FPT algorithm for vertex cover as a DPLL
procedure for Parameterized Resolution, we devise a proof search algorithm for Parameterized
Resolution and show that tree-like Parameterized Resolution allows short
refutations of all parameterized contradictions given as bounded-width CNF's.

Finally we show that the Pigeonhole Principle is difficult for dag-like
Parameterized Resolution, answering a question posed by Dantchev, Martin, and
Szeider. We generalize to the paremeterized case a lower bound technique
devised by Pudlak for Resolution.

The results presented are obtained in a sequence of joint work with Olaf
Beyersdorff and Massimo Lauria.

In the Max Acyclic Subdigraph problem we are given a digraph D and ask whether
D contains an acyclic subdigraph with at least k arcs. The problem is
NP-complete and it is easy to see that the problem is fixed-parameter tractable, i.e., there is an algorithm of running time f(k)n^{O(1)} for solving the problem, where f is a computable function of k only and n=|V(D)|. The last result
follows from the fact that the average number of arcs in an acyclic subdigraph
of D is m/2, where m is the number of arcs in D. Thus, it is natural to ask
another question: does D have an acyclic subdigraph with at least m/2 + k arcs?
It was an open problem [Mahajan, Raman and Sikdar (2006, 2009)] to establish
parameterized complexity of this problem and we can show that the problem is fixed-parameter tractable and has a quadratic kernel.

In fact, the Max Acyclic Subdigraph problem is the only nontrivial binary
Permutatation CSP parameterized above average. There are 62 nontrivial ternary
Permutation CSPs parameterized above average and we can show that all of them are fixed-parameter tractable and have kernels with quadratic number of variables. The 62 problems include Betweenness parameterized above average whose
complexity was stated as an open problem in the 2006 book by Niedermeier (where it is attributed to Benny Chor).

These results were obtained in joint papers with L. van Iersel, E.J. Kim, M. Mnich, S. Szeider, and A. Yeo. The tools we use include probabilistic inequalities and Hypercontractive Inequality.

One of the great success areas of parameterized algorithmics is that
of FPT algorithms running on tree-shaped decompositions of graphs
(utilizing width measures such as tree-width, branch-width,
clique-width, and rank-width). The problems solvable in such a way
primarily include those expressible in a suitable dialect of MSO logic.
While usual expositions of these (MSO based) algorithmic frameworks
involve decomposition methods from logic (e.g. Courcelle, Makowsky)
or MSO interpretations (e.g. Seese et al), we explain another approach
pioneered by Abrahamson and Fellows in the early 90's.

This alternative view is based on the classical Myhill-Nerode theorem
for finite tree automata and offers a precise mathematical
(combinatorial) description of the "states" a dynamic programming
algorithm has to process on a decomposition ("parse tree") of the input
graph in order to solve the specific problem. We shall demonstrate this
approach on the remarkably successful rank-width measure which has
emerged just in the past decade, and show a particular application
to the #SAT problem.

Several forms of reasoning - like abduction, closed world reasoning,
answer set programming, or belief revision - are well known to be
intractable. In fact, many of the relevant problems are on the second
or even third level of the polynomial hierarchy. The concept of
treewidth allows us to define tractable fragments of these problems,
i.e., all these problems become tractable (actually, even solvable in
linear time), if the treewidth of the involved formulae or programs is
bounded by some constant.

The proof of these tractability results is via Courcelle's Theorem or
extensions thereof. Of course, these tractability results as such do
not immediately yield feasible algorithms. However, several new,
custom-made algorithms have been recently developed for some of the
aforementioned reasoning tasks. They are based on a dynamic
programming approach and work by a bottom-up traversal of a tree
decomposition of the formula or program. Prototype implementations
have verified that these algorithms indeed work efficiently in case of
low treewidth.

Propositional modal logic can be considered as an extension of propositional logic with modal operators. Modal formulas may be satisfied by Kripke structures, a generalization of satisfying assignments of propositional logic formulas. In general, the satisfiability problem for modal logic is PSPACE-complete. This complexity may vary if we impose restrictions on the Kripke structures considered. We generalize incidence graphs that are usually associated with Constraint Satisfaction Problems to modal logic formulas in Conjunctive Normal Form. We present some results concerning the parameterized complexity of satisfiability of modal formulas with the treewidth of the incidence graph as a parameter. Another parameter we consider is the modal depth, which is also known to affect the complexity of modal satisfiability. For various restrictions of Kripke structures considered popularly in the literature, we give FPT or W[1]-hardness results.

The talk will report on some recent results on the parameterized complexity of
Constraint Satisfaction for multiple global All-Different constraints, in the
presence of various combinations of variable and value convexity, parameterized in various ways (e.g., maximum constraint size or maximum domain size).
Convexity refers to the setting where the variables (or values) are linearly
ordered, and the constraints consist of intervals of these. One of our main
results shows that the problem is fixed-parameter tractable when the
constraints are convex, parameterized by the maximum constraint size.

(Joint work with: Mike Fellows, Tobias Friedrich, Danny Hermelin and
Nina Narodytska.)

Last modified: 6 Sep 2010 by Stefan Szeider | W3C HTML4 Validator | W3C CCS Validator