Elementary Loops Revisited

The notions of loops and loop formulas play an important role in answer set computation. However, there would be an exponential number of loops in the worst case. Gebser and Schaub characterized a subclass elementary loops and showed that they are sufficient for selecting answer sets from models of a logic program. This paper proposes an alternative definition of elemen-tary loops and identify a subclass of elementary loops, called proper loops. By applying a special form of their loop formulas, proper loops are also sufficient for the SAT-based answer set computation. A polynomial algo-rithm to recognize a proper loop is given and shows that for certain logic programs, identifying all proper loops of a program is more efficient than that of elementary loops. Furthermore, we prove that, by considering the structure of the positive body-head dependency graph of a program, a large number of loops could be ignored for identifying proper loops. We provide another algo-rithm for identifying all proper loops of a program. The experiments show that, for certain programs whose de-pendency graphs consisting of sets of components that are densely connected inside and sparsely connected outside, the new algorithm is more efficient