title: Disjunctive answer set programming with backjumping and learning
Creators: name: Kammerhofer, Isabella
Publisher: name: TU Wien
Year: 2020
Subjects: subject: Abstract Solvers
subject: Answer-Set Prorgamming

description: Pseudocode wird in der Literatur häufig verwendet, um Solver oder Algorithmen zu beschreiben und miteinander zu vergleichen. Alternativ dazu kann auch ein so genanntes abstraktes Framework konstruiert werden. Dieses basiert auf Transitionssystemen. Niewenhuis, Oliveras und Tinelli (2006) führten diese Methode ein, um den Davis-Putnam-Logemann-Loveland-Algorithmus, einen Algorithmus zum Erfüllbarkeitsproblem der Aussagenlogik (SAT), zu modellieren und zu analysieren. Die Verwendung abstrakter Frameworks ist eine effektive Methode, mit der bestimmte Eigenschaften wie Endlichkeit, Azyklizität und Korrektheit analysiert, verglichen und bewiesen werden können. Brochenin, Lierler und Maratea (2015) griffen diese Idee auf, um sie auf disjunktives Answer Set Programming anzuwenden. Darüber hinaus konstruierten die Autoren ein generalisiertes Template, das eine Vielzahl möglicher Answer Set Solvers gleichzeitig erfasst. Ihre bisherige Arbeit beschränkte sich jedoch auf disjunktive Answer Set Solver mit Backtracking. Dabei sind die Solver, die sie in ihrer Arbeit erwähnt hatten, mit weiteren Methoden ausgestattet, die in der Arbeit nicht berücksichtigt wurden. Zu diesen Methoden gehören Backjumping, Learning, Forgetting und Restarting. In der vorliegenden Diplomarbeit werden wir einen Schritt weiter gehen und die Arbeit von Brochenin, Lierler und Maratea (2015) um diese weit verbreiteten Techniken erweitern. Wir zeigen, wie ein abstraktes Framework auf diversen, häufig verwendeten Answer Set Solvern aussieht, die die genannten Regeln Backjumping, Learning, Forgetting und Restarting verwenden. Da wir auf die frühere Arbeit aufsetzen, werden wir mit den Solvern cmodels, gnt und dlv arbeiten, wo wir die zusätzlichen Techniken erfassen. Wir werden auch das generalisierte Template erweitern und uns mit diversen Eigenschaften beschäftigen, die diese Solver mit sich bringen.
description: Pseudocodes are often used in literature to describe and compare solvers or algorithms. Alternatively, we can take the approach of constructing an abstract framework using transition systems. Nieuwenhuis, Oliveras and Tinelli (2006) introduced this method to model and analyse the Davis-Putnam-Logemann-Loveland algorithm for propositional satisfiability. Using abstract frameworks is an effective way to analyse, compare and prove specific features like finiteness, acyclicity and even correctness. Brochenin, Lierler and Maratea (2015) picked up that idea to apply it to disjunctive answer set solvers. Additionally, the authors created a general framework that captures a multitude of possible answer set solvers. The work was restricted to disjunctive answer set solvers with backtracking even though some of the solvers that were being mentioned in their work implement the more general and advanced methods of backjumping and learning, as well as forgetting and restarting. Therefore, we will go a step further and extend their work to these widely used techniques. We illustrate how an abstract framework looks on various commonly used answer set solvers that work with backjumping, learning, forgetting and restarting. Extending the earlier work, we will work with the solvers cmodels, gnt and dlv, where we will capture backjumping, learning, forgetting and restarting. We will also extend the general template from the earlier work and observe the earlier mentioned features from a more general point of view.