Christian Drescher, Martin Gebser, Torsten Grote, Benjamin Kaufmann, Arne König, Max Ostrowski, Torsten Schaub
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.
Subjects: 3. Automated Reasoning; 3.3 Nonmonotonic Reasoning
Submitted: Jun 13, 2008