Conflict-Driven Disjunctive Answer Set Solving

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

This page is copyrighted by AAAI. All rights reserved. Your use of this site constitutes acceptance of all of AAAI's terms and conditions and privacy policy.