Declarative and Computational Properties of Logic Programs with Aggregates

Abstract

We investigate the properties of logic programs with aggregates. We mainly focus on programs with monotone and antimonotone aggregates (LPA m,a programs). We define a new notion of unfounded set for LPA m,a programs, and prove that it is a sound generalization of the standard notion of unfounded set for aggregate-free programs. We show that the answer sets of an LPA m,a program are precisely its unfounded-free models. We define a well-founded operator WP for LPA m,a programs; we prove that its total fixpoints are precisely the answer sets of P, and its least fixpoint Wω P (∅) is contained in the intersection of all answer sets (if P admits an answer set). Wω P (∅) is efficiently computable, and for aggregate-free programs it coincides with the well-founded model. We carry out an in-depth complexity analysis in the general framework, including also nonmonotone aggregates. We prove that monotone and antimonotone aggregates do not increase the complexity of cautious reasoning, which remains in co-NP. Nonmonotone aggregates, instead, do increase the complexity by one level in the polynomial hierarchy. Our results allow also to generalize and speedup ASP systems with aggregates.