Fixed parameter algorithms for answer set programming

Abstract

Answer Set Programming (ASP) hat sich in den letzten Jahren als geeignete Methode etabliert, um kombinatorische Probleme zu lösen. ASP Programme lassen sich jedoch nur mit großem Aufwand berechnen. Zu ermitteln ob ein ASP Programm widerspruchsfrei ist, ist auf der zweiten Stufe der polynomiellen Hierarchie. Die parameterisierte Komplexitätstheorie ist ein vielversprechender Ansatz, allgemein schwer berechenbare Probleme zu behandeln. Hierbei wird nicht nur die Größe des Problems, sondern auch ein weiterer Wert, der Problemparameter, betrachtet. Einige Probleme sind leicht berechenbar wenn man den Problemparameter beschränkt, diese werden parametrisierbar genannt. Ein solcher Parameter ist die Baumbreite. Sie gibt an wie stark ein Graph einem Baum entspricht. ASP Programme können als Graphen dargestellt werden und besitzen daher eine Baumbreite. Mit Hilfe von monadischer Logik zweiter Ordnung und Courcelle's Theorem wurde bewiesen, dass der Test auf Widerspruchsfreiheit eines ASP Programms parametrisierbar ist.<br />Die Auswertung von monadischer Logik zweiter Ordnung (via Baumautomaten) ist jedoch nicht praktikabel, daher war dieses Ergebnis bisher nur von theoretischem Interesse. Wir stellen einen praktischen Algorithmus vor, der effizient ermittelt ob ein parametrisierbares ASP Programm widerspruchsfrei ist. Weiters geben wir Algorithmen an, die die Anzahl der Lösungen eines ASP Programms berechnen und alle Lösungen aufzählen.<br />Mit Hilfe dynamischer Programmierung stellen wir in linearer Zeit fest, ob ein parametrisierbares ASP Programm widerspruchsfrei ist. Unter der Annahme, dass arithmetische Operationen und Mengenoperationen jeweils nur eine Zeiteinheit benötigen, berechnen wir in linearer Zeit wieviele Lösungen es gibt, und, dass beim Aufzählen aller Lösungen die Wartezeit zwischen zwei Lösungen linear in der Größe der Probleminstanz beschränkt ist. Anhand einer prototypischen Implementierung können wir experimentell bestätigen, dass wir für Baumbreiten bis zu sechs, sehr gute Laufzeiten beim Zählen der Lösungen haben. Der direkte Vergleich mit einem aktuellen ASP System zeigt, dass die Laufzeit beim Aufzählen aller Lösungen kompetitiv ist. Lediglich der Test auf Widerspruchsfreiheit liegt hinter aktuellen Systemen.

Answer Set Programming (ASP) has gained much interest in the last decade and is an increasingly acknowledged paradigm for solving combinatorial problems. In general, determining whether an ASP program has at least one solution, that is, the ASP consistency problem, is already on the second level of the polynomial hierarchy. Parameterized complexity is a promising approach to deal with such intractable problems. It considers the problem-complexity not only as a function of the problem size, but also an additional problem-parameter. Hard problems may become tractable, if this problem-parameter is bounded by a fixed constant, they are then called fixed parameter tractable. One such parameter is treewidth, it measures how close a graph resembles a tree.<br />ASP programs can be encoded as graphs and have a treewidth. Using this approach, ASP consistency has been shown to be fixed parameter tractable via monadic second order logic and Courcelle's Theorem. Since the evaluation of monadic second order logic formulae (via tree automata) proved unpractical, this result was only of theoretical value. In this thesis, we propose practical algorithms to efficiently solve the ASP consistency problem. Additionally two more algorithms for problems of ASP, namely the counting problem (compute the number of solutions) and enumeration problem (compute each solution) are shown. Our dynamic programming algorithms solve the ASP consistency problem in linear time.<br />Further, assuming unit cost for arithmetic and set operations, the number of solutions can be computed in linear time, and the enumeration problem is shown to have linear delay. That is, the time between two solution is linearly bounded by the size of the problem instance.<br />Finally, our experiments with a prototype implementation show unprecedented performance for the counting problem. For the enumeration problem, our implementation is comparable to state of the art ASP solvers for a treewidth up to six, only for the ASP consistency problem, we significantly lie behind standard solvers.