KR Conference 2008 Conference Paper
Conflict-Driven Disjunctive Answer Set Solving
- Christian Drescher
- Martin Gebser
- Torsten Grote
- Benjamin Kaufmann
- Arne Koenig
- 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.