The paper presents two equivalent definitions of answer sets for logic programs with aggregates. These definitions build on the notion of unfolding of aggregates, and they are aimed at creating methodologies to translate logic programs with aggregates to normal logic programs or positive programs, whose answer set semantics can be used to defined the semantics of the original programs. The first definition provides an alternative view of the semantics for logic programming with aggregates described by The second definition is similar to the traditional answer set definition for normal logic programs, in that, given a logic program with aggregates and an interpretation, the unfolding process produces a positive program. The paper shows how this definition can be extended to consider aggregates in the head of the rules. The proposed views of logic programming with aggregates are simple and coincide with the ultimate stable model semantics, and with other semantic characterizations for large classes of program (e.g., programs with monotone aggregates and programs that are aggregate-stratified). Moreover, it can be directly employed to support an implementation using available answer set solvers. The paper describes a system, called ASP^A, that is capable of computing answer sets of programs with arbitrary (e.g., recursively defined) aggregates.
Let us consider the weight constraints employed by Smodels and let us describe a translation method to convert them into our language with aggregates. We will focus on weight constraint that are used in the body of rules (see Sect. for aggregates in the heads of rules). For simplicity, we will also focus on weight constraints with non-negative weights (the generalization can be obtained through algebraic manipulations, as described in @cite_36 ). A weight constraint @math has the form: Note that grounding removes Smodels ' conditional literals. [ L p_1 = w_1, ,p_n = w_n,not :r_1 = v_1, ,not :r_m = v_m U ] where @math are ground atoms, and @math are numeric constants. @math 's and @math 's are called literals of @math . @math denotes the set of literals of @math . The local weight function of a constraint @math , @math , returns the weight of its literals. For example, @math and @math . The weight of a weight constraint @math in a model @math , denoted by @math , is given by [ W(c,S) = p lit(c), : p S w(c)(p) + not :q lit(c), : q S w(c)(not :p). ]
@cite_36
2011124182
A novel logic program like language, weight constraint rules, is developed for answer set programming purposes. It generalizes normal logic programs by allowing weight constraints in place of literals to represent, e.g., cardinality and resource constraints and by providing optimization capabilities. A declarative semantics is developed which extends the stable model semantics of normal programs. The computational complexity of the language is shown to be similar to that of normal programs under the stable model semantics. A simple embedding of general weight constraint rules to a small subclass of the language called basic constraint rules is devised. An implementation of the language, the SMODELS system, is developed based on this embedding. It uses a two level architecture consisting of a front-end and a kernel language implementation. The front-end allows restricted use of variables and functions and compiles general weight constraint rules to basic constraint rules. A major part of the work is the development of an efficient search procedure for computing stable models for this kernel language. The procedure is compared with and empirically tested against satisfiability checkers and an implementation of the stable model semantics. It offers a competitive implementation of the stable model semantics for normal programs and attractive performance for problems where the new types of rules provide a compact representation.