Conflict-driven disjunctive answer set solving
Christian Drescher, Martin Gebser, Torsten Grote, Benjamin Kaufmann, Arne König, Max Ostrowski, Torsten H. Schaub · 2008
We elaborate a uniform approach to computing answer sets of disjunctive logic programs based on state-of-theart 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 Σ P 2-complete problems, taking advantage of Boolean constraint solving technology without using any legacy solvers as black boxes.