Backdoors to tractability of disjunctive answer set programming

Abstract

Antwortmengen-Programmierung (ASP) ist ein zunehmend populäres deklarative Programmierkonzept, welches die Modellierung von Problemen mit Hilfe logischer Programme erlaubt. Logische Programme bestehen aus Atomen, Regeln und Bedingungen, ihre Lösungen werden Antwortmengen genannt. Viele Probleme der künstlichen Intelligenz, wie beispielsweise nicht-monotones Schließen, können direkt in ASP formuliert werden. In dieser Arbeit beschäftigen wir uns vorrangig mit Schlussfolgerungsproblemen von ASP, beispielsweise die Fragestellung ob ein Programm mindestens eine Antwortmenge besitzt oder ob ein vorgegebenes Atom in mindestens einer Antwortmenge enthalten ist. Zentraler Gegenstand der gesamten Dissertation sind sogenannte aussagenlogische, disjunktive Programme. Die meisten ASP-Probleme sind schwer zu lösen, in der Komplexitätstheorie sind diese Probleme bekannt als vollständig für die zweite Stufe der polynomiellen Hierarchie. In dieser Arbeit lösen wir diese schweren Probleme mit Hilfe von sogenannten Hintertüren (Backdoors), die sich in Probleminstanzen finden lassen. Dabei kann eine günstige Hintertür für das Schlussfolgern als eine geschickte Abkürzung durch den Lösungsraum angesehen werden, die es ermöglicht das Problem in der Praxis schnell zu lösen. Die Größe der kleinsten Hintertür liefert uns darüber hinaus ein theoretisches Maß für die Schwierigkeit oder Einfachheit einer Probleminstanz. Das Grundprinzip einer Hintertür wurde bereits vielfältig in theoretischen Untersuchungen für das aussagenlogischen Erfüllbarkeitsproblem und das Bedingungserfüllungsproblem verwendet. In dieser Arbeit zeigen wir, dass das Prinzip einer Hintertür erfolgreich auf ASP übertragen werden kann. Wir entwickeln eine umfassende Theorie für ASP Hintertüren. Wir führen eine detaillierte asymptotische Komplexitätsanalyse durch, die ASP-Hintertüren mit einbezieht. Wir stellen neue Algorithmen vor, mit denen man kleine Hintertüren in Probleminstanzen erkennen und ausnutzen kann. Unsere Algorithmen erlauben es Probleminstanzen, die eine kleiner Hintertür besitzen, schnell zu lösen oder signifikant zu vereinfachen. Genauer, gewisse Hintertüren erlauben es uns Schlussfolgerungsprobleme von ASP effizient für Probleminstanzen, die eine kleine Hintertür besitzen, zu lösen (Parametrisierbarkeit); andere Hintertüren erlauben es uns dagegen Probleminstanzen, die eine kleine Hintertür besitzen, signifikant zu vereinfachen (komplexitätsbarrierebrechende Reduktionen); wiederum andere Hintertüren können aus theoretischer Sicht nicht genutzt werden, um Probleminstanzen effizient zu lösen oder zu vereinfachen (Schwierigkeit). Unsere komplexitätsbarrierebrechende Reduktionen liefern insbesondere für Probleminstanzen, die eine kleiner Hintertür besitzen, einen Ansatz die Grenze zwischen der zweiten Stufe der polynomiellen Hierarchy und der ersten Stufe zu durchbrechen und die betrachteten Probleme mit etablierten Methoden effektiver zu lösen. Darüber hinaus erarbeiten wir einen detaillierten Vergleich, in dem wir die Größe verschiedener Arten von Hintertüren miteinander in Beziehung setzen. Wir zeigen, dass das Prinzip einer Hintertür als vereinheitlichendes System für aus der Literatur bekannte Restriktionen, unter denen ASP-Probleme signifikant vereinfacht werden können, dienen kann.

Answer set programming (ASP) is an increasingly popular framework for declarative programming that admits the description of problems by means of atoms, rules, and constraints that form a logic program. The solutions of an answer set program are called answer sets. Many problems in artificial intelligence such as non-monotonic reasoning can be directly formulated in ASP. Reasoning problems for propositional disjunctive programs, which is the focus of this thesis, are of high computational complexity. For instance, the problems of deciding whether a program has at least one answer set or whether a given atom is contained in at least one answer set, are complete for the second level of the Polynomial Hierarchy. In this thesis we tackle these hard problems using backdoors in problem instances, which are sets of atoms that can be used as clever reasoning shortcuts through the search space. The concept of backdoors has widely been used in theoretical investigations in the areas of propositional satisfiability and constraint satisfaction, we show that backdoors can be fruitfully adapted to ASP. We develop a rigorous theory of backdoors for ASP and carry out a fine-grained asymptotic computational complexity analysis that takes backdoors into account. We establish new algorithms that can detect and take advantage of small backdoors to solve or to significantly simplify problem instances. More precisely, certain backdoors allow us to solve Asp reasoning problems efficiently for instances with small backdoors (fixed-parameter tractability), other backdoors allow us to significantly simplify the problem instance (complexity barrier breaking reduction), and some backdoors cannot even be used to simplify the problem instance (intractability). Particularly, our simplifications break the complexity barrier between the second level of the Polynomial Hierarchy and the first level by means of reductions that work efficiently for instances with small backdoors. Further, we elaborate upon a detailed comparison where we compare the size of certain types of backdoors with each other. We show that backdoors can serve as a unifying framework for restrictions that have been identified in the literature under which ASP problems significantly simplify and become tractable or NP-complete.