Completion of Disjunctive Logic Programs

Abstract

Clark's completion plays an important role in ASP computation:it discards unsupported models via unit resolution; hence, it improves the performance of ASP solvers, and at the same time it simplifies their implementation. In the disjunctive case, however, Clark's completion is usually preceded by another transformation known as shift, whose size is quadratic in general. A different approach is proposed in this paper: Clark's completion is extended to disjunctive programs without the need of intermediate program rewritings such as the shift. As in the non-disjunctive case, the new completion is linear in size, and discards unsupported models via unit resolution. Moreover, an ad-hoc propagator for supported model search is presented. PDF