Conflict-Driven Disjunctive Answer Set Solving

We elaborate a uniform approach to computing answer sets of disjunctive logic programs based on state-of-the-art Boolean constraint solving techniques. Starting from a constraint-based characterization of answer sets, we develop advanced solving algorithms, featuring backjumping and conflict-driven learning using the First-UIP scheme as well as sophisticated unfounded set checking. As a final result, we obtain a competitive solver for $Sigma_2^P$-complete problems, taking advantage of Boolean constraint solving technology without using any legacy solvers as black boxes.

Authors

• Christian Drescher NICTA and University of New South Wales
• Martin Gebser University of Klagenfurt Graz University of Technology
• Torsten Grote
• Benjamin Kaufmann University of Potsdam
• Arne Koenig
• Max Ostrowski
• Torsten Schaub

Keywords

No keywords are indexed for this paper.