Mitarbeiterseminar Logik in der Informatik

Abstract State Machines (kurz ASMs) sind ein prominenter Vertreter für die Spezifikation und Verifikation von Hard- und Software. In der Logik stellen sie für die Beschreibung von Strukturklassen ein neues, interessantes Berechnungsmodell zur Verfügung. In dieser Arbeit werden ASMs als eine Art Programmiersprache für Strukturen aufgefasst. Dabei wurden die Programme so entworfen, dass natürliche Einschränkungen in der Syntax und Semantik das Einfangen von klassischen Komplexitätsklassen auf endlichen, geordneten Strukturen erlaubt. Im Vortrag wird anhand von altbekannten Logiken gezeigt welche ASM-Programme die Komplexitätsklassen LOGSPACE und PTIME einfangen.

Motiviert durch einen Beweis eines starken Karp-Lipton Kollapses in beschränkter Arithmetik haben Cook und Krajicek 2007 aussagenlogische Beweissysteme mit Advice definiert. Die Beweislängen solcher Systeme korrespondieren, analog zu den klassischen Systemen von Cook und Reckhow, mit Kollapskonsequenzen der Polynomiellen Hierarchie.

Ich werde einen Überblick über die bisherigen Ergebnisse auf diesem Gebiet geben. Insbesondere werden wir uns der Frage der (p)-Optimalität solcher Systeme innerhalb ihrer eigenen Klasse, wie auch Simulationseigenschaften gegenüber schwächeren Beweissystemen annehmen. Danach werden wir uns noch kurz mit der (schwierigeren) Frage der Beschränktheit der Beweislängen solcher Systeme beschäftigen.

Recently Fortnow and Santhanam showed that NP-hard problems do not have so-called distillations unless the polynomial hierarchy collapses. This lemma has proven useful in many respects. For example Bodlaender, Downey, Fellows and Hermelin based on it a method to exclude polynomial kernelizations for parameterized problems. The talk presents refinements of the lemma making it useful also in other respects. Concerning PCP systems the lemma can be used to establish lower bounds on the number of new variables that have to be introduced in gap amplifications for SAT. Another application concerns Buhrmans and Hitchcocks recent lower bound on the density of NP-hard problems.

The maximum constraint satisfaction problem (Max CSP)
provides a unified framework which can express
many combinatorial optimisation problems including Max Cut and Max
k-Sat. An instance of Max CSP consists of a
collection of weighted constraints on overlapping sets of variables,
and the goal is to find values for the variables that
maximise the total weight of simultaneously satisfied constraints. We
will consider the problem of determining how exactly
the complexity and approximability of Max CSPs depend on the type of
constraints allowed in instances. We will discuss
the recently discovered strong link between tractability of Max CSPs
and supermodular functions defined on products of lattices, and
present some classification results based on this link.

Separation Logic is both an assertion language that may express some properties of memory states, and a Hoare-like proof system for programs manipulating pointers, the former being intensively used in the latter. This logic has been actively popularized by the "London Massive" team (Peter O'Hearn, Hongseok Yang, Cristiano Calcagno, Dino Di Stefano).

In the first part of my presentation, I will present a personnal, brief survey on pointer programs verification, and introduce the essentials of the separation logic approach. The second part will be more personnal and technical, I will focus on the assertion language and review some of our recent results on decidability and expressiveness issues.

On the decidability side, I will present decidable classes that are not (yet) handled by the automatic tools developed by the "London Massive" team : data-aware logics, and unrestricted first-order quantification. These results allow to prove, for instance, that merging two ordered lists gives an ordered list.

On the expressiveness side, I will explain the roles played by the two specific separation logic connectives : separating conjunction and magic-wand (joint work with Stéphane Demri and Remi Brochenin). It will be presented in particular that the magic-wand subsumes the separating conjunction, and provides an expressive power equivalent to *full* second-order logic. Of other interest is that separating conjunction alone fits into *monadic* second-order logic, the strict inclusion being still a conjecture, although it is known that it encodes MSO over words.

Maschinelle Lernverfahren werden in verschiedenen Bereichen wie Data Mining oder der Künstlichen Intelligenz eingesetzt. Dabei werden für verschiedene Lernprobleme unterschiedliche Algorithmen entworfen, die meist auf statistischen Methoden beruhen. Ein Lernproblem unter vielen ist die Konzeptlernaufgabe bei der unbekannte Konzepte anhand von Beispielen möglichst genau erlernt werden soll. Im Rahmen der algorithmischen Lerntheorie wird das Konzeptlernen vorgestellt. Der Parameter der Vapnik-Chervonenkis-Dimension wird hierbei eine wichtige Rolle spielen. Denn mithilfe der VC-Dimension können Komplexitätsaussagen hinsichtlich der Konzeptklassen getroffen werden, und es wird sich ferner herausstellen, dass mithilfe der VC-Dimension effizient erlernbare Konzeptklassen charakterisiert werden können. Als Abschluss des Vortrages wird das Ergebnis vorgestellt, dass die VC-Dimension auf der Klasse der Bäume beschränkt ist.

Das hier untersuchte Problem wird als Häufige-Sequenzen Problem bezeichnet und besteht darin in einer Menge von Sequenzen (Sequenz-Datenbank) alle (Sub-)Sequenzen, die öfter als ein vorher bestimmter Schwellenwert vorkommen, zu finden. Dabei wird gezählt in wie vielen Sequenzen der Datenbank eine (Sub-)Sequenz vorkommt unabhängig davon, wie oft diese in den einzelnen Sequenzen der Datenbank vorkommt.
Im gängigen Verständnis ist eine Sequenz eine Menge von Elementen in einer festen Reihenfolge, z. B. ist ein Wort eine Sequenz von Buchstaben. In dem hier untersuchten Problem bestehen die Elemente der Sequenzen wiederum aus Mengen von Elementen, die Itemsets genannt werden.
Weiterhin wird hier auf der Gesamtzahl aller Items, die in den Itemsets einer Sequenz vorkommen können, eine Ordnung angenommen, nach der die Items in einem Itemset angeordnet sind. In einem Itemset tritt jedes Item höchstens einmal auf.
Wenn man aus einer Sequenz Items löscht, ohne die Reihenfolge der übrigen Items zu verändern erhält man eine Subsequenz dieser Sequenz. Werden alle Items eines Itemsets gelöscht, so kann es ganz weggelassen werden.
Es wird gezeigt, dass das Häufige-Sequenzen Entscheidungsproblem NP-vollständig ist. Von verschiedenen Algorithmen, die zur Lösung des Häufige-Sequenzen Problem entwickelt wurden, wird der SPAM-Algorithmus näher vorgestellt und gezeigt, dass dieser Algorithmus polynomial delay erfüllt, d. h. zwischen jeder Ausgabe einer häufigen Sequenz vergeht Polynomzeit in der Größe der Eingabe.
In weiteren Untersuchungen sollen Varianten des Häufige-Sequenzen Problems betrachtet werden, z. B. als Parametrisierungs- und Optimierungsprobleme.

Modern SAT solvers have seen huge efficiency gains over the last decade. Being well optimized implementations of the DPLL algorithm they are widely used in many applications. Among these are, for example, microporocessor verification and bounded model checking, which often require the solution of inputs with hundreds of thousands of variables.

The fact that SAT solvers are indeed able to handle such situations apparently conflicts with the well known intractability of the SAT problem. Recent approaches by Beame, Kautz, Sabharwal and Bacchus, Hertel, Pitassi and Van Gelder have tried to get a proof complexity theoretic account of this phenomenon.

In a different direction we propose a more algorithmic view, relating efficient solvability by a SAT solver to bounded width resolution. Among other things this enables us to show that SAT solvers are able to handle CNF formulas of bounded treewidth in polynomial time.

This is joint work with Albert Atserias.

Datalog ist die relationale Variante der logischen Programmierung und ist eine Standard-Abfragesprache in der Datenbankentheorie geworden. Die Programmkomplexität von Datalog im bisherigen Hauptanwendungsgebiet, auf endlichen Strukturen, ist bekanntermaßen in EXPTIME. Wir untersuchen die Komplexität von Datalog auf unendlichen Strukturen, motiviert durch mögliche Anwendungen von Datalog auf unendlichen Strukturen (z.B. linearen Ordnungen) im zeitlichen und räumlichen Schliessen, aber auch durch das aufkommende Interesse an unendlichen Strukturen bei verwandten theoretischen Problemen, wie Constraint Satisfaction Problems (CSP):

Im Gegensatz zu endlichen Strukturen können Datalog-Berechnungen auf unendlichen Strukturen unendlich lange dauern, was zur Unentscheidbarkeit von Datalog auf unendlichen Strukturen führen kann. Aber auch in den entscheidbaren Fällen kann die Komplexität von Datalog auf unendlichen Strukturen beliebig hoch sein. Im Hinblick auf dieses Ergebnis widmen wir uns dann unendlichen Strukturen mit der niedrigsten Komplexität von Datalog: Wir zeigen, dass Datalog auf linearen Ordnungen (auch dichte und diskrete, mit oder ohne Konstanten und sogar gefärbte) und Baumordnungen EXPTIME-vollständig ist.

Für die Bestimmung der oberen Schranke werden Werkzeuge für Datalog auf Ordnungen eingeführt: Ordnungstypen, Abstandstypen und typdisjunkte Programme. Die Typkonzepte liefern eine endliche Beschreibung der unendlichen Programmergebnisse und könnten auch für praktische Anwendungen von Interesse sein. Wir erzeugen spezielle typdisjunkte Programme, die sich ohne Rekursion lösen lassen.

Ein Transfer unserer Methoden auf CSPs zeigt, dass CSPs auf unendlichen Strukturen mit beliebig hoher Zeitkomplexität vorkommen, wie bei Datalog.

For every relational structure B, the (non-uniform) constraint satisfaction problem associated to B, CSP(B), is the following computational problem: given a relational structure A, is there a homomorphism from A to B?. The complexity of the problem CSP(B) varies depending on the election of the structure B. In the last few years much effort has been invested in the project of classifying the computational complexity of CSP(B), for every B. An useful tool in this study has been the consideration of the logics that can express CSP(B). Perhaps the best illustration of this approach is the fact that a good number of the tractable cases of the problem identified so far can be explained, in an uniform way, as those CSP(B) definable in Datalog. During the first half of the talk we shall survey the connection between definability in several fragments of Datalog and the existence of obstruction sets. During the second half of the talk we shall focus on those structures with an obstruction set consisting only of trees, where we shall present some recent results.