Loops: Relevant or redundant?

Abstract

Loops and the corresponding loop formulas play an important role in answer set programming. On the one hand, they are used for guaranteeing correctness and completeness in SAT-based answer set solvers. On the other hand, they can be used by conventional answer set solvers for finding unfounded sets of atoms. Unfortunately, the number of loops is exponential in the worst case. We demonstrate that not all loops are actually needed for answer set computation. Rather, we characterize the subclass of elementary loops and show that they are sufficient and necessary for selecting answer sets among the models of a program's completion. Given that elementary loops cannot be distinguished from general ones in atom dependency graphs, we show how the richer graph structure provided by body-head dependency graphs can be exploited for this purpose. © Springer-Verlag Berlin Heidelberg 2005.