Physical Sciences and Mathematics Commons^™

Abstract Disjunctive Answer Set Solvers, Remi Brochenin, Yuliya Lierler, Marco Maratea

Computer Science Faculty Proceedings & Presentations

A fundamental task in answer set programming is to compute answer sets of logic programs. Answer set solvers are the programs that perform this task. The problem of deciding whether a disjunctive program has an answer set isΣ^P₂ -complete. The high complexity of reasoning within disjunctive logic programming is responsible for few solvers capable of dealing with such programs, namely DLV, GNT, CMODELS and CLASP. We show that transition systems introduced by Nieuwenhuis, Oliveras, and Tinelli to model and analyze satisfiability solvers can be adapted for disjunctive answer set solvers. In particular, we present transition systems for CMODELS …