1: \documentclass{tlp}
2: \usepackage{aopmath}
3:
4: \newtheorem{definition}{Definition} % [section]
5: \newtheorem{example}{Example} % [section]
6: \newtheorem{remark}{Remark} % [section]
7:
8: \usepackage{epsfig}
9: \usepackage{url}
10: \usepackage{amsfonts}
11: \usepackage{latexsym}
12:
13: \newcommand{\uffa}{\mbox{$\: {\tt : \!\! - }\:$}}
14: \newcommand{\CASP}{${ASP}^A$}
15: \newcommand{\assi}{\#\!\!=}
16: \newcommand{\mydot}{\textit{.}}
17:
18: \def\qed{\hfill{$\Box$}}
19: \def\naf{ not \;}
20:
21: \submitted{17 June 2005 }
22: \revised{27 October 2005}
23: \accepted{13 January 2006}
24:
25: \title[A Constructive Semantic Characterization of Aggregates
26: in ASP]
27: {A Constructive Semantic Characterization of Aggregates
28: in Answer Set Programming}
29:
30: \author[Tran Cao Son and Enrico Pontelli]
31: {TRAN CAO SON and ENRICO PONTELLI\\
32: Department of Computer Science\\
33: New Mexico State University\\
34: \{tson,epontell\}@cs.nmsu.edu}
35:
36: \begin{document}
37:
38: \maketitle
39:
40: \begin{abstract}
41: This technical note describes a monotone and
42: continuous fixpoint operator
43: to compute the answer sets of programs with aggregates.
44: The fixpoint operator
45: relies on the notion of
46: {\em aggregate solution}.
47: Under certain conditions, this operator behaves identically
48: to the three-valued immediate consequence operator
49: $\Phi^{aggr}_P$ for aggregate programs, independently
50: proposed in~\cite{Pelov04,PelovDB04}.
51: This operator allows us to closely tie the
52: computational complexity of the answer set checking
53: and answer sets existence problems
54: to the cost of checking a solution of the aggregates
55: in the program. Finally, we relate the semantics described
56: by the operator to other proposals for
57: logic programming with aggregates.
58: \end{abstract}
59: \begin{keywords}
60: Aggregates, answer set programming, semantics
61: \end{keywords}
62:
63:
64: \section{Introduction}
65: Several semantic characterizations of answer sets of logic
66: programs with aggregates have been proposed
67: over the years (e.g.,
68: \cite{KempS91,MumickPR90,a-prolog,faberLP04,PelovDB04}).
69: Most of these proposals have their roots in the
70: answer set semantics of normal logic programs
71: without aggregates \cite{GL88}. Nevertheless,
72: it is known that a straightforward
73: generalization of the definition of answer sets to programs with
74: aggregates may yield {\em non-minimal} and/or
75: unintuitive answer sets. Consider the
76: following example.
77:
78: \begin{example} \label{exp2}
79: Let $P$ be the program
80: \[
81: \begin{array}{lcl}
82: p(1) \leftarrow & \hspace{1cm} &
83: p(2) \leftarrow \hspace{4cm}
84: p(3) \leftarrow \\
85: p(5) \leftarrow q &&
86: q \leftarrow \textnormal{\sc Sum}(\{X \mid p(X)\}) > 10
87: \end{array}
88: \]
89: The aggregate $ \textnormal{\sc Sum}(\{X \mid p(X)\}) > 10$
90: is satisfied by any interpretation $M$ of $P$
91: where the sum of $X$ such that
92: $p(X)$ is true in $M$ is greater than 10.
93:
94: A straightforward extension of the original definition of
95: answer sets~\cite{GL88} defines $M$ to be
96: an answer set of $P$ if and only if $M$ is the minimal
97: model of the reduct $P^M$, where $P^M$ is the program
98: obtained by {\em (i)} removing from $P$ all the rules containing in their
99: body at least an aggregate or a negation-as-failure literal which
100: is false in $M$; and {\em (ii)} removing all the aggregates
101: and negation-as-failure literals from the remaining rules.
102: Effectively, this definition treats aggregates in the same
103: fashion as negation-as-failure literals.
104:
105: It is easy to see that for
106: $A = \{p(1),p(2),p(3)\}$ and $B = \{p(1),p(2),p(3),p(5),q\}$, \[
107: \begin{array}{lll}
108: P^A = \left\{
109: \begin{array}{l}
110: p(1) \leftarrow \\
111: p(2) \leftarrow \\
112: p(3) \leftarrow \\
113: p(5) \leftarrow q \\
114: \end{array}
115: \right \}
116: & \hspace*{0.5cm} &
117: P^B = \left \{
118: \begin{array}{l}
119: p(1) \leftarrow \\
120: p(2) \leftarrow \\
121: p(3) \leftarrow \\
122: p(5) \leftarrow q \\
123: q \leftarrow \\
124: \end{array}
125: \right \}
126: \end{array}
127: \]
128: and $A$ and $B$ are minimal model of $P^A$
129: and $P^B$ respectively. Thus, both $A$ and $B$ are
130: answer sets of $P$. As we can see, treating
131: aggregates like negation-as-failure literals
132: yields non-minimal answer sets. Accepting $B$ as an
133: answer set seems counter-intuitive, since $p(5)$ ``supports''
134: itself through the aggregate.
135: \qed
136: \end{example}
137: Different approaches have been proposed to deal with this problem. Early works
138: concentrate on finding syntactic (e.g., stratification
139: \cite{MumickPR90,KempS91}) and semantic (e.g., monotonic aggregates
140: \cite{RossS97,KempS91})
141: restrictions on aggregates
142: which guarantee minimality, and often uniqueness, of answer sets.
143:
144:
145: In this technical note, we present a fixpoint operator that allows
146: us to compute answer sets of normal logic programs with
147: {\em arbitrary aggregates}.
148: It is a straightforward extension of the Gelfond-Lifschitz definition,
149: making use of the \emph{same} notion of reduct as in \cite{GL88}, and
150: relying on a continuous fixpoint operator for computing
151: selected minimal models of the reduct (corresponding to
152: our notion of answer sets). This fixpoint operator is a
153: natural extension of the traditional
154: immediate consequence operator $T_P$ to programs with aggregates.
155: It takes into consideration
156: the provisional answer set while trying to verify that it is
157: an answer set. This fixpoint operator makes use of
158: the notion of \emph{aggregate solutions}, and it
159: captures the
160: \emph{unfolding semantics} for normal logic programs with
161: aggregates, originally proposed in~\cite{ElkabaniPS04} and completely
162: developed in~\cite{SonPE05}. This semantics builds on the principle
163: of unfolding of intensional set constructions, as developed
164: in~\cite{DovierPR01}.
165: This operator corresponds to the $\Phi_P^{aggr}$ operator proposed
166: in~\cite{PelovDB04,Pelov04}, when ultimate approximating
167: aggregates are employed and 2-valued stable models are considered.
168: In particular, the two operators are identical when they are applied
169: to the construction of a correct answer set $M$.
170:
171: The proposed fixpoint operator allows us also to easily
172: demonstrate the existence of a
173: large class of logic programs with aggregates
174: (which includes recursively defined aggregates
175: and non-monotone aggregates)
176: for which the problems of answer set checking and of
177: determining the existence of an answer set is in {\bf P} and
178: {\bf NP} respectively.
179: Finally, we relate our work to recently proposed
180: semantics for programs with aggregates
181: \cite{faberLP04,PelovDB04,SonPE05}.
182:
183:
184: \section{Preliminary Definitions}
185: \label{sec2}
186:
187: \subsection{Language Syntax}
188: Let us consider a signature
189: $\Sigma_L = \langle {\cal F}_L\cup {\cal F}_{Agg}, {\cal V}\cup {\cal V}_l, \Pi_L \rangle$,
190: where ${\cal F}_L$ is a
191: collection of constants, ${\cal F}_{Agg}$ is a collection of
192: unary function symbols,
193: ${\cal V} \cup {\cal V}_l$ is a denumerable collection of variables
194: (such that ${\cal V} \cap {\cal V}_l = \emptyset$),
195: and $\Pi_L$ is a collection of predicate symbols. In the rest of this paper, we
196: will always assume that the set $\mathbb{Z}$ of the integers is
197: a subset of ${\cal F}_L$---i.e., there are distinct constants representing the
198: integer numbers.
199: We will refer to $\Sigma_L$ as the \emph{ASP signature}.
200: We will also refer to
201: $\Sigma_P = \langle {\cal F}_P,{\cal V}\cup {\cal V}_l, \Pi_P\rangle$
202: as the \emph{program signature},
203: where ${\cal F}_P \subseteq {\cal F}_L$, $\Pi_P \subseteq \Pi_L$, and
204: ${\cal F}_P$ is finite.
205: We will denote
206: with ${\cal H}_P$ the $\Sigma_P$-Herbrand universe, containing
207: the ground terms built using symbols
208: of ${\cal F}_P$, and
209: with ${\cal B}_P$ the corresponding $\Sigma_P$-Herbrand base. An
210: ASP-atom is an atom of the form
211: $p(t_1,\dots,t_n)$,
212: where $t_i \in {\cal F}_P \cup {\cal V}$
213: and $p\in \Pi_P$; an ASP-literal is either an ASP-atom
214: or the negation as failure ($not\:A$) of an ASP-atom.
215: We will use the traditional notation $\{t_1,\dots,t_k\}$ to denote an
216: extensional set of terms, and the notation
217: $\{\!\!\{t_1,\dots,t_k\}\!\!\}$ to denote an
218: extensional multiset (or bag) of terms.
219:
220: \begin{definition}[Intensional Sets and Multisets]
221: \label{intensionalset}
222: An \emph{intensional set} is a set of the form
223: $ \{X \:\mid\: p(X_1,\dots,X_k)\} $
224: where $X\in {\cal V}_l$, $X_i$'s are variables or constants
225: (in ${\cal F}_P$),
226: $\{X_1,\dots,X_k\} \cap {\cal V}_l = \{X\}$,
227: and $p$ is a $k$-ary predicate in $\Pi_P$.
228: Similarly, an \emph{intensional multiset} is a multiset
229: of the form
230: $$
231: \{\!\!\{ X \:\mid\: \exists Z_1,\dots,Z_r \mydot\:
232: p(Y_1,\dots,Y_m)\}\!\!\}
233: $$
234: where $\{X,Z_1,\dots,Z_r\}\subseteq {\cal V}_l$, $Y_i$ are variables
235: or constants (of ${\cal F}_P$),
236: $\{Y_1,\ldots,Y_m\} \cap {\cal V}_l= \{X,Z_1,\dots,Z_r\}$,
237: and $X \notin \{Z_1,\dots,Z_r\}$.
238: We call $X$ the \emph{grouped variable},
239: $Z_1,\dots,Z_r$ the \emph{local variables},
240: and $p$ the \emph{grouped predicate} of the intensional set/multiset.
241: \end{definition}
242: Intuitively, in an intensional multiset, we collect
243: the values of $X$ for which $p(Y_1,\ldots,Y_m)$ is true, under the
244: assumptions that the variables $Z_1,\dots,Z_r$ are locally,
245: existentially quantified. Multiple
246: occurrences of the same value of $X$ can appear. For example, if
247: $p(X,Z)$ is true for $X=1, Z=2$ and $X=1, Z=3$, then the multiset
248: $\{\!\{X\mid\exists Z. p(X,Z)\}\!\}$ will correspond to $\{\!\!\{1,1\}\!\!\}$.
249: %
250: Definition \ref{intensionalset} can be easily extended
251: to allow more complex types of sets, e.g., sets with
252: a tuple as the grouped variable and sets with conjunctions of atoms
253: as property of the intensional construction.
254:
255: Observe that the variables from ${\cal V}_l$ are used exclusively
256: as grouped or local variables in defining intensional sets/multisets, and
257: they cannot occur anywhere else.
258:
259: We write $\bar{X}$ to denote $X_1,\ldots,X_n$.
260:
261: %
262: \begin{definition}[Aggregate Terms/Atoms]
263: \begin{itemize}
264: \item
265: An \emph{aggregate term} is of the form $aggr(s)$, where $s$ is
266: an intensional set/multiset, and $aggr \in {\cal F}_{Agg}$ (called the
267: \emph{aggregate function}).
268:
269: \item
270: An \emph{aggregate atom} has the form
271: $aggr(s) \:\: \texttt{op} \:\: Result$,
272: where {\tt op} is a relational
273: operator in the set $\{=, \neq, <, >, \leq, \geq\}$ and
274: $Result \in {\cal V} \cup (\mathbb{Z} \cap {\cal F}_P)$---i.e.,
275: it is either a variable or a numeric constant.
276: \end{itemize}
277: \end{definition}
278: %
279: In our examples, we will focus on the traditional aggregate functions, e.g.,
280: {\sc Count, Sum, Min}.
281: For an aggregate atom $\ell$ of the form $aggr(s) \:\: \texttt{op} \:\: Result$,
282: we refer to the grouped variable and predicate of $s$
283: as the grouped variable and predicate of $\ell$.
284: The set of ASP-atoms constructed from the grouped predicate of $\ell$ and
285: the terms in ${\cal H}_P$ is denoted by
286: ${\cal H}(\ell)$.
287: %A variable
288: %$X$ is a {\em free variable} in $\ell$ if {\em (i)} $X$ occurs in $s$
289: %and it differs from the grouped and local variables of $\ell$;
290: %or {\em (ii)} $Result$ is a variable and $X$ is identical to $Result$.
291: %$\ell$ is a ground aggregate atom if it does not
292: %contain any free variable.
293:
294: \begin{definition}
295: [\CASP\ Rule/Program]
296: \begin{itemize}
297: \item An \CASP\ rule is of the form
298: %
299: \begin{equation} \label{agg-rule}
300: A \leftarrow C_1,\ldots,C_m,A_1,\ldots,A_n,\naf B_1, \dots, \naf B_k
301: \end{equation}
302: %
303: where $A$, $A_1$, $\dots$, $A_n$, $B_1$, $\dots$, $B_k$ are ASP-atoms, while
304: $C_1, \dots, C_m$ are aggregate atoms ($m\geq 0$, $n\geq 0$, $k\geq 0$).
305:
306: \item
307: An \CASP\ program is a finite collection of \CASP\ rules.
308: \end{itemize}
309: \end{definition}
310: For an \CASP\ rule $r$ of the form (\ref{agg-rule}),
311: $head(r)$, $agg(r)$, $pos(r)$, and
312: $neg(r)$ denote respectively $A$, $\{C_1, \ldots, C_m\}$,
313: $\{A_1, \ldots, A_n\}$, and $\{B_1, \ldots, B_k\}$.
314: Furthermore, $body(r)$ denotes the right-hand side
315: of the rule $r$.
316:
317: Observe that grouped and local variables in an aggregate atom
318: $\ell$ have a scope limited to $\ell$. As such, given an \CASP\ rule,
319: it is always possible to rename such variables occurring in
320: the aggregate atoms $C_1,\ldots,C_m$ apart,
321: so that they are pairwise different. Observe also that the
322: grouped and local variables represent the only occurrences
323: of variables from ${\cal V}_l$, thus they will not
324: occur in $A$, $A_1$, $\dots$, $A_n$, $B_1$, $\ldots$, $B_k$.
325: For this reason, without loss of generality,
326: whenever we refer to an \CASP\ rule $r$, we will assume
327: that the grouped and local variables of its aggregate atoms are
328: pairwise different and do not appear in the rest of the rule.
329:
330: Given a term, literal, aggregate atom, rule $\alpha$, let
331: us denote with $fvars(\alpha)$ the set
332: of variables from ${\cal V}$ present in $\alpha$. The entity
333: $\alpha$ is ground
334: if $fvars(\alpha) = \emptyset$.
335:
336: A ground substitution $\sigma$ is a set $\{X_1/c_1,\ldots,X_n/c_n\}$
337: where $X_i$'s are distinct variables from ${\cal V}$
338: and $c_i$'s are constants in ${\cal F}_P$.
339: For an ASP-atom $p$ (an aggregate atom $\ell$),
340: $p \sigma$ ($\ell \sigma$) denotes the ASP-atom
341: (the aggregate atom) which is obtained from
342: $p$ ($\ell$) by simultaneously replacing
343: every occurrence of $X_i$ with $c_i$.
344:
345: Let $r$ be a rule of the form (\ref{agg-rule}) and
346: $\{X_1,\ldots,X_t\}$ be the set of free variables occurring in
347: $A$, $C_1,\ldots,C_m$,
348: $A_1,\ldots,A_n$, and $B_1,\ldots,B_k$---i.e.,
349: $fvars(r) = \{X_1,\dots,X_t\}$.
350: Let $\sigma$ be a ground substitution $\{X_1/c_1,\ldots,X_t/c_t\}$.
351: The ground instance of $r$ w.r.t. $\sigma$,
352: denoted by $r\sigma$,
353: is the ground rule obtained from $r$ by simultaneously replacing
354: every occurrence of $X_i$ with $c_i$.
355:
356: By $ground(r)$
357: we denote the set of all ground instances of the rule $r$. For a program $P$,
358: the set of all ground instances
359: of the rules in $P$, denoted by $ground(P)$, is called the ground
360: instance of $P$, i.e.,
361: $ground(P) = \bigcup_{r \in P} ground(r)$.
362:
363:
364: \subsection{Aggregate Solutions}
365:
366: In this subsection we provide the basic definitions of satisfaction and
367: solution of an aggregate atom.
368: %We make use of the usual
369: %notion of interpretation~\cite{lloyd}, i.e.,
370: %an interpretation of an \CASP\ program $P$ on $\Sigma_P$
371: %is a set of ASP-atoms from ${\cal B}_P$.
372: %We also use the traditional notation $I\models a$ to denote
373: %the fact that the ASP-atom $a$ is true in the interpretation
374: %$I$---i.e., $a \in I$.
375: \begin{definition}[Interpretation Domain and Interpretation]
376: The domain of our interpretations is the set
377: ${\cal D} = {\cal H}_P \cup 2^{{\cal H}_P} \cup {\cal M}({\cal H}_P)$, where
378: $2^{{\cal H}_P}$ is the set of (finite) subsets of ${\cal H}_P$ and
379: ${\cal M}({\cal H}_P)$ is the set of finite multisets of elements
380: from ${\cal H}_P$.
381: An interpretation $I$ is a pair $\langle {\cal D}, (\cdot)^I\rangle$, where
382: $(\cdot)^I$ is a function that maps ground terms to elements of $\cal D$ and ground
383: atoms to truth values.
384: \end{definition}
385:
386: \begin{definition}[Interpretation Function]
387: Given a constant $c$, its interpretation $c^I$ is equal to $c$.
388:
389: \smallskip
390: \noindent
391: Given a ground intensional set $s$ of the form $\{X \mid p(\bar{X})\}$,
392: its interpretation $s^I$
393: is the set $\{a_1,\dots,a_n\} \subseteq {\cal H}_P$, where
394: $(p(\bar{X}))\{X / a_i\}^I$ is equal to true for
395: $1\leq i\leq n$, and no other value for $X$ has such property.
396:
397: \smallskip
398: \noindent
399: Given a ground intensional multiset $s$ of the form
400: $\{\!\!\{X\:\mid\: \exists \bar{Z}\mydot p(\bar{X},\bar{Z})\}\!\!\}$,
401: its interpretation $s^I$ is the multiset
402: $\{\!\!\{a_1,\dots,a_k\}\!\!\} \in {\cal M}({\cal H}_P)$
403: where, for each $1\leq i\leq k$,
404: there is a ground substitution $\eta_i$ for $\bar{Z}$ such that
405: $p(\bar{X},\bar{Z})\gamma_i^I$ is true for
406: $\gamma_i = \eta_i \cup \{X/a_i\}$, and no other elements
407: satisfy this property.
408:
409: \smallskip
410: \noindent
411: Given the aggregate term $aggr(s)$, its interpretation is
412: $aggr^I(s^I)$, where
413: $$aggr^I: 2^{ {\cal H}_P }\cup {\cal M}({ {\cal H}_P }) \rightarrow \mathbb{Z}.$$
414:
415: \smallskip
416: \noindent
417: Given a ground \CASP\ atom $p(t_1,\dots,t_n)$, its interpretation is
418: $p^I(t_1^I,\dots,t_n^I)$, where $p^I: {\cal D}^n \rightarrow \{\texttt{true},\texttt{false}\}$.
419:
420: \smallskip
421: \noindent
422: Given a ground aggregate atom
423: $\ell$ of the form $aggr(s) \; {\tt op} \; Result$, its
424: interpretation
425: $\ell^I$ is true if
426: $op^I(aggr(s)^I,Result^I)$ is true, where
427: ${\tt op}^I: \mathbb{Z} \times \mathbb{Z} \rightarrow \{\texttt{true},\texttt{false}\}$.
428: \end{definition}
429: We will assume that the traditional aggregate functions
430: are interpreted in the usual way. E.g., {\sc Sum}$^I$
431: is the function that
432: maps a set/multiset of numbers to its sum, and
433: {\sc Count}$^I$ is the function that maps a set/multiset
434: of constants to its cardinality. Similarly, we assume that
435: the traditional relational operators (e.g., $\leq$, $\neq$) are
436: interpreted according to their traditional meaning.
437:
438: Given a literal $not\:p$, its interpretation
439: $(not\:p)^I$ is true (false) iff $p^I$ is false (true).
440:
441: Given an atom, literal, or aggregate atom $\ell$,
442: we will denote with $I\models \ell$ the fact that
443: $\ell^I$ is true.
444:
445: \begin{definition}[Rule Satisfaction]
446: $I$ {\em satisfies the body of a ground rule} $r$
447: (denoted by $I \models body(r)$), if
448: \begin{list}{}{\topsep=0pt \itemsep=1pt \parsep=0pt}
449: \item[(i)] $pos(r) \subseteq I$;
450: \item[(ii)] $neg(r) \cap I = \emptyset$;
451: \item[(iii)] $I \models c$ for every $c \in agg(r)$.
452: \end{list}
453: $I$ {\em satisfies a ground rule} $r$ if $I \models head(r)$ or
454: $I \not\models body(r)$.
455: \end{definition}
456: % %
457: Having specified when an interpretation satisfies an aggregate atom
458: or a \CASP\ rule, we can define the notion of model of a program.
459: %
460: \begin{definition}[Model]
461: Let $P$ be an \CASP\ program. An interpretation $M$ is
462: a {\em model} of $P$ if $M$ satisfies every rule in $ground(P)$.
463: \end{definition}
464: In our view of interpretations, we assume that the interpretation
465: of the aggregate functions and relational operators is fixed. In this
466: perspective, we will still be able to keep the traditional view of
467: interpretations as subsets of ${\cal B}_P$.
468:
469: \begin{definition}
470: $M$ is a \emph{minimal model} of $P$ if $M$ is a model of $P$ and
471: there is no proper subset of $M$ which is also a model of $P$.
472: \end{definition}
473:
474:
475: We will now define a notion called {\em aggregate solution}.
476: Observe that the satisfaction of
477: an ASP-atom $a$ is \emph{monotonic}, in the sense that if
478: $I \models a$ and $I \subseteq I'$ then we have that $I' \models a$.
479: On the other hand, the satisfaction of an aggregate atom is possibly
480: non-monotonic, i.e., $I \models \ell$
481: and $I \subseteq I'$ do not necessarily imply $I' \models \ell$.
482: For example, $\{p(1)\} \models \textnormal{\sc Sum}(\{X \mid p(X)\}) \ne 0$
483: but $\{p(1),p(-1)\} \not\models
484: \textnormal{\sc Sum}(\{X \mid p(X)\}) \ne 0$.
485: The notion of aggregate solution allows us to
486: define an operator where
487: the monotonicity of satisfaction of aggregate
488: atoms is used in verifying an answer set.
489: %
490: \begin{definition}[Aggregate Solution]
491: Let $\ell$ be a ground aggregate atom.
492: An {\em aggregate solution} of $\ell$ is a pair $\langle S_1, S_2 \rangle$ of
493: disjoint subsets of ${\cal H}(\ell)$ such that, for every interpretation $I$,
494: if $S_1 \subseteq I$ and
495: $S_2 \cap I = \emptyset$ then
496: $I \models \ell$.
497: ${\cal SOLN}(\ell)$ is the set of all the solutions
498: of $\ell$.
499: \end{definition}
500: %
501: It is obvious that
502: if $I \models \ell$ then $\langle I \cap {\cal H}(\ell),
503: {\cal H}(\ell) \setminus I \rangle$
504: is a solution of $\ell$.
505: Let $S = \langle S_1, S_2 \rangle$ be an aggregate
506: solution of an aggregate atom;
507: we denote with $S\mydot p$ and $S\mydot n$ the two components
508: $S_1$ and $S_2$ of the solution.
509: %
510:
511: \begin{example} \label{ex-sol}
512: Consider the aggregate atom
513: ${\textnormal{\sc Sum}(\{X \mid p(X)\}) > 10}$ from the program
514: in Example \ref{exp2}. This atom has a unique solution:
515: $\langle \{p(1), p(2), p(3), p(5)\}, \emptyset\rangle$.
516: On the other hand, the aggregate atom
517: ${\textnormal{\sc Sum}(\{X \mid p(X)\}) > 6}$ has
518: the following solutions:
519: \[
520: \begin{array}{lrclr}
521: \langle \{p(3), p(5)\}, &\emptyset\rangle & \hspace{.8cm} &
522: \langle \{p(3), p(5)\}, &\{p(1),p(2)\}\rangle \\
523: \langle \{p(3), p(5)\}, &\{p(1)\}\rangle & &
524: \langle \{p(3), p(5)\}, &\{p(2)\}\rangle \\
525: \langle \{p(2), p(5)\}, &\emptyset\rangle & &
526: \langle \{p(2), p(5)\}, &\{p(1),p(3)\}\rangle \\
527: \langle \{p(2), p(5)\}, &\{p(1)\}\rangle & &
528: \langle \{p(2), p(5)\}, &\{p(3)\}\rangle \\
529: \langle \{p(1), p(2), p(5)\}, &\emptyset\rangle & &
530: \langle \{p(1), p(2), p(5)\}, &\{p(3)\}\rangle \\
531: \langle \{p(1), p(3), p(5)\}, &\emptyset\rangle & &
532: \langle \{p(1), p(3), p(5)\}, &\{p(2)\}\rangle \\
533: \langle \{p(1), p(2), p(3), p(5)\}, &\emptyset\rangle & &
534: \langle \{p(2), p(3), p(5)\}, &\emptyset\rangle \\
535: \langle \{p(2), p(3), p(5)\}, &\{p(1)\}\rangle \\
536: \end{array}
537: \]
538: \qed\end{example}
539: %
540:
541: %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
542:
543: \section{A Fixpoint Operator based on Aggregate Solutions}
544: \label{semantics}
545:
546: In this section, we construct the semantics for
547: \CASP\ programs, through the use of a monotone and
548: continuous fixpoint operator.
549: For the sake of simplicity,
550: we will assume that programs, ASP-atoms,
551: and aggregate atoms referred to in this section
552: are ground\footnote{
553: A program $P$ with variables can be viewed as a shorthand
554: for $ground(P)$.
555: }.
556: As we will show in Section~\ref{pelov}, this fixpoint operator
557: behaves as the 3-valued immediate consequence operator of
558: \cite{PelovDB04} under certain conditions (e.g., use of
559: ultimate approximating aggregates).
560:
561: \begin{definition}[Reduct for \CASP\ Programs]
562: Let $P$ be an \CASP\ program and let $M$ be an interpretation.
563: The reduct of $P$ with respect to $M$, denoted by $^M\!P$, is defined as
564: \[
565: ^M\!P=\left\{ head(r) \leftarrow pos(r),agg(r) \mid
566: r \in ground(P), \;\;
567: M \cap neg(r) = \emptyset
568: \right\}
569: \]
570: \end{definition}
571: Observe that, for a program $P$ without aggregates, the process
572: of checking whether $M$ is an answer set \cite{GL88}
573: requires first computing
574: the Gelfond-Lifschitz reduct of $P$ w.r.t. $M$ ($P^M$), and then
575: verifying that $M$ is the least model of $P^M$.
576: This second step is performed by using
577: the van Emden-Kowalski operator $T_{P^M}$ to regenerate $M$,
578: by computing the least fixpoint of $T_{P^M}$. I.e.,
579: we compute the sequence $M_0, M_1, M_2, \dots$ where
580: $M_0 = \emptyset$ and $M_{i+1} = T_{P_M}(M_i)$.
581: In every step of regenerating $M$, an atom $a$
582: is added to $M_{i+1}$ iff there is a rule in $P^M$ whose head is
583: $a$ and whose body is contained in $M_i$.
584: This process is monotonic, in
585: the sense that, if $a$ is added to $M_i$, then $a$ will belong to $M_j$ for
586: all $j \ge i$.
587:
588: Our intention is to define a $T_P$-like operator for programs with aggregates.
589: Specifically, we would like to verify that
590: $M$ is an answer set of $P$ by generating a monotone
591: sequence of interpretations
592: $M_0 \subseteq M_1 \subseteq \ldots \subseteq M_n \subseteq \ldots = M$.
593: To do so, we need to specify when a rule of $^M\!P$ can be used,
594: i.e., when an ASP/aggregate atom is considered satisfied by $M_i$.
595: We also need to ensure that, at each step $i+1$,
596: $M_{i+1}$ will {\em still} satisfy all ASP-atoms and
597: the aggregate atoms that are satisfied by $M_{i}$.
598:
599: This observation leads us to define the notion of \emph{conditional
600: satisfaction} of an atom (ASP-atom or aggregate atom) over
601: a pair of sets of atoms $(I,M)$---where $I$ is an interpretation
602: generated at some step of the verification process,
603: and $M$ is the answer set that needs to be verified.
604:
605: \begin{definition}[Conditional Satisfaction] \label{cond-sat}
606: Let $\ell$ be an ASP-atom or an aggregate atom,
607: and $I$, $M$ be two interpretations\footnote{
608: Recall that an interpretation is a set of atoms in ${\cal B}_P$.
609: }. We define the
610: \emph{conditional satisfaction} of $\ell$ w.r.t. $I$ and $M$, denoted by
611: $(I,M) \models \ell$, as:
612: \begin{list}{$\bullet$}{\topsep=1pt \parsep=0pt \itemsep=1pt}
613: \item if $\ell$ is ASP-atom, then
614: $(I,M) \models \ell \:\:\Leftrightarrow\:\:I\models \ell$
615:
616: \item if $\ell$ is an aggregate atom, then
617: \[ (I,M) \models l \:\:\Leftrightarrow\:\:
618: \langle I\cap M\cap {\cal H}(\ell),\: {\cal H}(\ell)\setminus M\rangle
619: \textit{ is a solution of $\ell$}\]
620: \end{list}
621: \end{definition}
622: %
623: The first bullet says that an ASP-atom is satisfied by a pair $(I,M)$ if it is
624: satisfied by $I$. The second bullet states that
625: $I$ contains enough information of $M$ to guarantee that any successive
626: expansion of $I$ towards $M$ will satisfy the aggregate.
627: Conditional satisfaction is naturally
628: extended to conjunctions of atoms.
629: The following lemma trivially holds.
630: \begin{lemma} \label{l0}
631: Let $\ell$ be an ASP-atom or an aggregate atom
632: and $I, J, M$ be interpretations such that
633: $I \subseteq J$. Then, $(I,M) \models \ell$ implies $(J,M) \models \ell$.
634: \end{lemma}
635: We are now ready to define the consequence operator for \CASP\
636: programs.
637:
638: \begin{definition}[Consequence Operator]
639: Let $P$ be an \CASP\ program
640: and $M$ be an interpretation.
641: We define the consequence operator on $P$ and $M$, called
642: $K_M^P$, as
643: \[
644: K_M^P(I) = \{\:head(r) \:\:\mid\:\: r\in {^M\!P}\:\wedge\: (I,M) \models body(r)\:\}
645: \]
646: for every interpretation $I$ of $P$.
647: \end{definition}
648: %
649: By definition, we have that $K_M^P(I) = T_P(I)$ for definite
650: programs without aggregate atoms. Thus, $K_M^P$ can be viewed
651: as an extension of
652: $T_P$ to the class of programs with aggregates.
653: The following lemma is a consequence of Lemma~\ref{l0}.
654: %
655: \begin{lemma} \label{l4}
656: Let $P$ be a program
657: and $M$ be an interpretation. Then,
658: $K_M^P$ is monotone and continuous over the lattice
659: $\langle 2^{{\cal B}_P}, \subseteq \rangle$.
660: \end{lemma}
661: The above lemma allows us to conclude that the least fixpoint of
662: $K_M^P$, denoted by $lfp(K_M^P)$, exists and it is equal to
663: $K_M^P \uparrow \omega$. Here,
664: $K^P_M \uparrow n$ denotes
665: $$\underbrace{K^P_M(K^P_M(\dots(K^P_M}_{n-times \; K^P_M}(\emptyset)\dots)))$$
666: and $K^P_M \uparrow \omega $ denotes
667: $\lim_{n \rightarrow \infty} K^P_M \uparrow n$.
668: We are now ready
669: to define the concept of \emph{answer set} of an \CASP\ program.
670:
671: \begin{definition}[Fixpoint Answer Set]
672: Let $P$ be an \CASP\ program and let $M$ be
673: an interpretation. $M$ is a \emph{fixpoint answer
674: set} of $P$ iff $M=lfp(K_M^P)$.
675: \end{definition}
676: %
677: Whenever it is clear from the context, we will simply talk about
678: \emph{answer sets} of $P$ instead of fixpoint answer sets.
679:
680: \begin{example} \label{exp4}
681: Let us continue with the program $P$ from Example \ref{exp2}.
682: Since $P$ does not contain negation-as-failure literals, $^M\!P = P$
683: for any interpretation $M$ of $P$.
684: Any answer set of $P$ must contain $p(1)$, $p(2)$, and
685: $p(3)$. We will now show that $A = \{p(1), p(2), p(3)\}$ is the
686: unique fixpoint answer set of $P$. It is easy to see that
687: %
688: \[
689: \begin{array}{lcl}
690: K_A^P \uparrow 0 & = & \emptyset\\
691: K_A^P \uparrow 1 & = & K_A^P (K_A^P \uparrow 0) = \{p(1), p(2), p(3)\} \\
692: K_A^P \uparrow 2 & = & \{p(1), p(2), p(3)\} = K_A^P \uparrow 1
693: \end{array}
694: \]
695: Thus, $A$ is indeed a fixpoint answer set of $P$.
696:
697: Let us consider $B = \{p(1), p(2), p(3),p(5), q\}$.
698: We have that $^B\!P = P$ and it is easy to verify that
699: $lfp(K_B^P) = \{p(1), p(2), p(3)\}$.
700: Therefore, $B$ is not a fixpoint answer set of $P$. It is easy to check
701: that no proper superset of $A$ is a fixpoint answer set of $P$, i.e., $A$ is
702: the unique answer set of $P$.
703: \qed
704: \end{example}
705: %
706: In the next example, we show how this definition works when the
707: programs contain negation-as-failure literals.
708: \begin{example}
709: Let $P$ be the program\footnote{
710: We would like to thank Vladimir Lifschitz for providing us this example.
711: }:
712: \[
713: \begin{array}{lll}
714: p(a) & \leftarrow & \textnormal{\sc Count}(\{X \mid p(X)\}) > 0 \\
715: p(b) & \leftarrow & \naf q \\
716: q & \leftarrow & \naf p(b) \\
717: \end{array}
718: \]
719: We will show now that the program has two answer sets $A = \{q\}$
720: and $B = \{p(b),p(a)\}$. We have that
721: \begin{itemize}
722: \item $^A\!P$ consists of the first rule and the fact
723: $q$. The verification that $A$ is an answer set of $P$ is shown next.
724: %
725: \[
726: \begin{array}{lcl}
727: K_A^P \uparrow 0 & = & \emptyset\\
728: K_A^P \uparrow 1 & = & K_A^P (K_A^P \uparrow 0) = \{q\}\\
729: K_A^P \uparrow 2 & = & \{q\} = K_A^P\uparrow 1
730: \end{array}
731: \]
732: $p(a)$ cannot belong to $K_A^P \uparrow 1$ since
733: $\langle \emptyset, \emptyset \rangle$ is not a solution of the
734: aggregate atom $\textnormal{\sc Count}(\{X \mid p(X)\}) > 0$.
735:
736: \item $^B\!P$ consists of the first rule and the fact
737: $p(b)$.
738: %
739: \[
740: \begin{array}{lcl}
741: K_B^P \uparrow 0 & = & \emptyset\\
742: K_B^P \uparrow 1 & = & K_B^P (K_B^P \uparrow 0) = \{p(b)\}\\
743: K_B^P \uparrow 2 & = & \{p(b),p(a)\} \\
744: K_B^P \uparrow 3 & = & \{p(b),p(a)\} = K_B^P \uparrow 2
745: \end{array}
746: \]
747: $p(a)$ belongs to $K_B^P \uparrow 2$ since
748: $\langle \{p(b)\}, \emptyset \rangle$ is a solution of the
749: aggregate atom $\textnormal{\sc Count}(\{X \mid p(X)\}) > 0$.
750: \end{itemize}
751: It is easy to see that $P$ does not have any other answer sets.
752: \qed
753: \end{example}
754:
755:
756: \section{Related Work and Discussion}
757: \label{discuss}
758:
759: In this section, we will relate our proposal to the unfolding
760: semantics presented in \cite{SonPE05} and to
761: two other recently proposed semantics for
762: programs with aggregates\footnote{
763: A detailed comparison between the semantics in \cite{SonPE05}
764: and earlier proposals for programs with aggregates
765: can be found in the same report.
766: }---i.e.,
767: the ultimate stable model semantics
768: \cite{PelovDB03,PelovDB04,Pelov04} and the minimal answer set semantics
769: \cite{faberLP04}. We will also investigate some of the computational
770: complexity issues related to
771: determining the fixpoint answer sets of \CASP\ programs.
772:
773: %In our proof, we write $T_P \uparrow n$ to denote
774: %$\underbrace{T_P(T_P(\dots(T_P}_{n-times \; T_P}(\emptyset)\dots)))$
775: %where $T_P$ is the van Emden -- Kowalski function defined for
776: %definite logic programs. Similarly,
777: %$T_P \uparrow \omega$ denotes the least fixpoint of $T_P$.
778:
779: \subsection{Equivalence of Fixpoint Semantics and Unfolding Semantics}
780: We will show that the notion of fixpoint answer set
781: corresponds to the {\em unfolding semantics}
782: presented in \cite{SonPE05}.
783: To make this note self-contained, let us
784: recall the basic definition of the unfolding semantics.
785: For a ground aggregate atom $c$ and an
786: interpretation $M$, let
787: $${\cal S}(c, M) = \left\{S_c
788: \:\mid\: S_c \in {\cal SOLN}(c),
789: \:S_c\mydot p \subseteq M,\: S_c \mydot n \cap M = \emptyset \right\}
790: $$
791: %
792: Intuitively, ${\cal S}(c, M)$ is the set of solutions of $c$
793: which are satisfied by $M$.
794: For a solution $S_c \in {\cal S}(c,M)$,
795: the unfolding of $c$ in $M$ w.r.t. $S_c$
796: %(denoted by $c_M(S_c)$)
797: is the conjunction $\bigwedge_{a \in S_c\mydot p} a$.
798: We say that $c'$ is an unfolding of $c$
799: with respect to $M$ if $c'$ is an unfolding of $c$ in $M$ with respect
800: to some $S_c \in {\cal S}(c, M)$. When
801: ${\cal S}(c, M) = \emptyset$, we say that $false$
802: is the unfolding of $c$ in $M$. The unfolding of
803: a rule $r \in ground(P)$ with respect to $M$
804: is the set of rules $unfolding(r,M)$ defined
805: as follows:
806: %
807: \begin{enumerate}
808: \item If
809: $neg(r) \cap M \ne \emptyset$ or
810: there is some $c \in agg(r)$
811: such that $false$ is the unfolding of $c$
812: in $M$
813: then $unfolding(r,M) = \emptyset$;
814: \item If $neg(r) \cap M = \emptyset$ and
815: $false$ is not the unfolding of $c$
816: for every $c \in agg(r)$,
817: then $r' \in unfolding(r,M)$ where
818: \begin{enumerate}
819: \item $head(r') = head(r)$
820: \item $neg(r') = neg(r)$
821: \item there is a sequence of aggregate solutions
822: $\langle S_c \rangle_{c \in agg(r)}$
823: for the aggregates in $agg(r)$,
824: such that $S_c \in {\cal S}(c,M)$ for every
825: $c \in agg(r)$ and
826: $pos(r') = pos(r) \cup \bigcup_{c \in agg(r)} S_c\mydot p$.
827: \end{enumerate}
828: \end{enumerate}
829: %
830: For a program $P$, $unfolding(P,M)$ denotes the set
831: of unfolding rules of $ground(P)$ w.r.t. $M$.
832: $M$ is an \CASP-answer set of $P$ iff
833: $M$ is an answer set of $unfolding(P, M)$.
834:
835: This notion of unfolding derives from the work on
836: unfolding of intensional sets~\cite{DovierPR01}, and has been
837: independently described in~\cite{PelovDB03}.
838:
839:
840: \begin{lemma}\label{l1}
841: Let $c$ be an aggregate atom, let $M$ be an interpretation,
842: and let $S_c$ be a solution of $c$ such that $S_c \in {\cal S}(c,M)$.
843: Then, $\langle S_c\mydot p, {\cal H}(c)\setminus M\rangle$ is a solution
844: of $c$.
845: \end{lemma}
846: \begin{proof}
847: Let us consider an interpretation $I$ such that
848: $S_c\mydot p \subseteq I$ and $I \cap ({\cal H}(c)\setminus M) = \emptyset$.
849: Because $S_c\mydot n \subseteq {\cal H}(c) \setminus M$,
850: $I \cap S_c\mydot n = \emptyset$. Since $S_c$ is a solution,
851: $I\models c$. Since this holds for every interpretation $I$
852: satisfying
853: $S_c\mydot p\subseteq I$ and $I \cap ({\cal H}(c)\setminus M) = \emptyset$,
854: we have that $\langle S_c\mydot p, {\cal H}(c)\setminus M\rangle$ is a solution
855: of $c$.
856: \end{proof}
857:
858: \begin{lemma} \label{l2}
859: Let $R=unfolding(P,M)$. Then
860: $T_R\uparrow i = K_M^P\uparrow i$ for $i\geq 0$.
861: \end{lemma}
862: \begin{proof}
863: Let us prove the result by induction on $i$.
864:
865:
866: \noindent
867: {\em Base:} for $i=0$, we have that $T_R \uparrow 0 = \emptyset = K_M^P\uparrow 0$,
868: and the result is obviously true.
869: Let us consider the case $i=1$.
870: \begin{itemize}
871: \item Let $p \in T_R\uparrow 1 = \{
872: \ell \:\mid\: (\ell\leftarrow) \in R\}$.
873: If $p\leftarrow$ is a fact in $P$, then it is also
874: a fact in $^M\!P$. This means that $p\leftarrow$ is an
875: element of $^M\!P$, and thus $p$ is in
876: $K_M^P\uparrow 1$.
877: Otherwise, there is a rule $r$ in $P$, such that
878: \begin{list}{-}{\topsep=1pt \parsep=0pt \itemsep=1pt}
879: \item $head(r) = p$;
880: \item $pos(r) = \emptyset$;
881: \item $neg(r) \cap M = \emptyset$; and
882: \item for each $\ell \in agg(r)$ we have that
883: there exists a solution of $\ell$ of the
884: form $\langle \emptyset,J\rangle$ such that
885: $M \cap J =\emptyset$.
886: \end{list}
887: The rule $p\leftarrow agg(r)$ is a
888: rule in $^M\!P$. From Lemma~\ref{l1} we can conclude
889: that $(\emptyset,M) \models agg(r)$, thus ensuring
890: that $p \in K^P_M\uparrow 1$.
891:
892: \item Let $p \in K^P_M\uparrow 1$. Thus, there exists
893: a rule $r'\in {^M\!P}$ such that $(\emptyset,M)\models body(r)$
894: and $head(r')=p$.
895: This means that there is a rule $r \in P$ such that
896: \begin{list}{-}{\topsep=1pt \parsep=0pt \itemsep=1pt}
897: \item $head(r) = head(r') = p$;
898: \item $M \cap neg(r) = \emptyset$;
899: \item $pos(r) = \emptyset$; and
900: \item $agg(r) = agg(r')$.
901: \end{list}
902: Since $(\emptyset,M) \models agg(r)$, we have that,
903: for each $c\in agg(r)$,
904: $\langle \emptyset, {\cal H}(c)\setminus M\rangle$ is
905: a solution of $c$. This means that the rule
906: $p \leftarrow $ is in $unfolding(P,M)$. This also means
907: that $p\in T_R\uparrow 1$.
908: \end{itemize}
909:
910:
911: \smallskip
912:
913: \noindent
914: \emph{Step:} Let us assume that the result holds for $i \leq k$ and
915: consider the iteration $k+1$.
916:
917: \begin{list}{$\bullet$}{\topsep=1pt \parsep=0pt \itemsep=1pt \leftmargin=10pt}
918: \item Let $p \in T_R\uparrow (k+1)$ and
919: $p \not\in T_R\uparrow k$.
920: Thus, there is a rule $r'$ in $R$ such
921: that
922: \begin{list}{-}{\topsep=1pt \parsep=0pt \itemsep=1pt}
923: \item $head(r')=p$; and
924: \item $pos(r') \subseteq T_R\uparrow k$.
925: \end{list}
926: This implies that there is a rule $r\in P$ such that
927: \begin{list}{-}{\topsep=1pt \parsep=0pt \itemsep=1pt}
928: \item $head(r) = p$;
929: \item $pos(r) \subseteq T_R\uparrow k$;
930: \item $M \cap neg(r) =\emptyset$; and
931: \item for each $c \in agg(r)$, there is a solution
932: $S_c$ s.t. $S_c\mydot p \subseteq T_R\uparrow k$
933: and $M \cap S_c\mydot n = \emptyset$.
934: \end{list}
935: This also means that
936: $p \leftarrow pos(r),agg(r)$ is a rule in
937: $^M\!P$.
938:
939: We already know that $pos(r) \subseteq K^P_M\uparrow k$.
940: Now we wish to show that $(K^P_M\uparrow k, M) \models agg(r)$.
941: Lemma \ref{l1} shows that, for each $c \in agg(r)$,
942: $\langle S_c\mydot p, {\cal H}(c)\setminus M\rangle$ is a solution of $c$.
943: This allows us to conclude that $p \in K^P_M\uparrow (k+1)$.
944:
945:
946: \item Let $p \in K^P_M\uparrow (k+1)$ and
947: $p \not\in K^P_M\uparrow k$.
948: This means that there is a rule $r'$ in $^M\!P$ such that
949: \begin{list}{-}{\topsep=1pt \parsep=0pt \itemsep=1pt}
950: \item $head(r') = p$;
951: \item $pos(r') \subseteq K^P_M\uparrow k$; and
952: \item $( K^P_M\uparrow k, M) \models body(r')$
953: \end{list}
954: This also means that there is a rule $r$ in $P$ such
955: that
956: \begin{list}{-}{\topsep=1pt \parsep=0pt \itemsep=1pt}
957: \item $head(r) = head(r') = p$;
958: \item $agg(r) = agg(r')$;
959: \item $pos(r) = pos(r')$;
960: \item $neg(r) \cap M = \emptyset$; and
961: \item for each $c \in agg(r)$,
962: $S_c = \langle K^P_M\uparrow k\cap M\cap {\cal H}(c),
963: {\cal H}(c) \setminus M \rangle$ is a
964: solution of $c$.
965: \end{list}
966: This means that there is a rule $r''$ in
967: $unfolding(P,M)$ such that:
968: \begin{list}{-}{\topsep=1pt \parsep=0pt \itemsep=1pt}
969: \item $head(r'') = p$
970: \item $pos(r'') = pos(r) \cup \bigcup_{c\in agg{r}} S_c\mydot p$
971: \end{list}
972: Since each $S_c\mydot p \subseteq K^P_M\uparrow k=T_R\uparrow k$
973: for each $c \in agg(r)$
974: and $pos(r) \subseteq K^P_M\uparrow k=T_R\uparrow k$,
975: we have that
976: $p \in T_R\uparrow (k+1)$.
977: \end{list}
978: \end{proof}
979:
980: \begin{theorem} \label{fixpointasp}
981: Let $P$ be a program with aggregates. $M$ is an answer set
982: of $unfolding(P,M)$ iff $M$ is a fixpoint answer set of $P$.
983: \end{theorem}
984: \begin{proof}
985: Let $R = unfolding(P,M)$. We have that
986: $M$ is an answer set of $P$ iff
987: $M = T_R\uparrow \omega$ iff
988: $M = K^P_M \uparrow \omega$ (Lemma \ref{l2}).
989: \end{proof}
990:
991: The results from~\cite{SonPE05} and Theorem~\ref{fixpointasp} provide us
992: a direct connection between fixpoint answer sets and other
993: semantics for logic programs with aggregates.
994:
995: \subsection{Faber et al.'s Minimal Model Semantics}
996: The notion of answer set proposed in \cite{faberLP04}
997: is based on a new notion of reduct, defined as follows.
998: Given a program $P$ and a set of ASP-atoms $M$,
999: the {\em reduct of P with respect to M}, denoted by
1000: $\Gamma(M,P)$, is obtained by removing from
1001: $ground(P)$ those rules whose body cannot be satisfied by $M$.
1002: In other words, $\Gamma(M,P) = \{r \mid r \in ground(P), M \models body(r)\}$.
1003:
1004:
1005: \begin{definition} [FLP-answer set, \cite{faberLP04}]
1006: \label{d-faberLP04}
1007: For a program $P$, $M$ is an {\em FLP-answer set} of $P$
1008: if it is a minimal model of $\Gamma(M,P)$.
1009: \end{definition}
1010: The following theorem derives directly from Theorem~\ref{fixpointasp} and
1011: \cite{SonPE05}.
1012:
1013: \begin{theorem}
1014: \label{th2}
1015: Let $P$ be a program with aggregates. If $M$ is a fixpoint answer set,
1016: then $M$ is an FLP-answer set of $P$.
1017: \end{theorem}
1018: Observe that there are cases where FLP-answer sets are not fixpoint answer
1019: sets.
1020:
1021: \begin{example}
1022: Consider the program $P$ where
1023: \[
1024: \begin{array}{lll}
1025: p(1)& \leftarrow & \textnormal{\sc Sum}(\{X \mid p(X)\}) \ge 0 \\
1026: p(-1)& \leftarrow & p(1) \\
1027: p(1)& \leftarrow & p(-1) \\
1028: \end{array}
1029: \]
1030: It can be checked that $M = \{p(1), p(-1)\}$ is an FLP-answer set of $P$.
1031: It is possible to show that
1032: $\textnormal{\sc Sum}(\{X \mid p(X)\}) \geq 0$ has the
1033: following solutions:
1034: $\langle \emptyset, \{p(1),p(-1)\} \rangle$,
1035: $\langle \{p(1)\}, \{p(-1)\} \rangle$,
1036: $\langle \{p(1)\}, \emptyset \rangle$, and
1037: $\langle \{p(1),p(-1)\}, \emptyset \rangle$.
1038:
1039: We have that $K^P_M(\emptyset) = \emptyset$ since
1040: $\langle \emptyset, \emptyset \rangle$ is not a solution
1041: of $\textnormal{\sc Sum}(\{X \mid p(X)\}) \ge 0$.
1042: This implies that $lfp(K^P_M) = \emptyset$.
1043: Thus, $M$ is not a fixpoint answer set of $P$.
1044: It can be easily verified that $P$ does not have any fixpoint answer
1045: set.
1046: \qed
1047: \end{example}
1048:
1049: \begin{remark}
1050: If we replace in $P$ the rule
1051: $p(1) \leftarrow \textnormal{\sc Sum}(\{X \mid p(X)\}) \ge 0$
1052: with the intuitively equivalent {\sc Smodels} weight constraint
1053: rule $$p(1) \leftarrow 0 [p(1) = 1, p(-1)=-1]$$
1054: we obtain a program that does not have answer sets
1055: in {\sc Smodels}.
1056: \end{remark}
1057:
1058: The above example shows that our characterization
1059: differs from \cite{faberLP04}. Our definition is closer to
1060: {\sc Smodels}' understanding of aggregates.
1061:
1062:
1063: \subsection{Approximation Semantics for Logic Programs with Aggregates}
1064: \label{pelov}
1065:
1066: The work of Pelov et al. \cite{PelovDB03,Pelov04,PelovDB04} contains an elegant
1067: generalization of several semantics of logic programs to logic
1068: programs with aggregates. The key idea in this work is the use of
1069: approximation theory in defining several semantics for logic programs
1070: with aggregates (e.g., two-valued semantics, ultimate three-valued stable
1071: semantics, three-valued stable model semantics).
1072: In particular, in \cite{PelovDB04}, the authors describe a fixpoint
1073: operator, called $\Phi^{appr}_P$, operating on 3-valued interpretations and
1074: parameterized by the choice of approximating aggregates.
1075:
1076:
1077:
1078: It is possible to show the following results:
1079: \begin{itemize}
1080: \item Whenever the approximating aggregate used in $\Phi^{appr}_P$
1081: is the \emph{ultimate approximating aggregate}~\cite{PelovDB04},
1082: then the fixpoint semantics defined by the
1083: operator $K^P_M$ coincides with the two-valued stable model semantics
1084: defined by the operator $\Phi^{appr}_P$.
1085: \item It is possible to prove a stronger result,
1086: showing that, if $I \subseteq M$
1087: then $K_M^P(I) = \Phi^{aggr,1}_P(I,M)$, where $\Phi^{aggr,1}_P(I,M)$
1088: denotes the first component of $\Phi^{aggr}_P(I,M)$. In other words,
1089: when ultimate approximating aggregates are employed and $M$ is an
1090: answer set, then the fixpoint
1091: operator of Pelov et al. and
1092: $K_M^P$ behave identically.
1093: \end{itemize}
1094: We will prove next the first of these two results. The proof of the
1095: second result (kindly contributed by one of the anonymous reviewers)
1096: can be found in Appendix A.
1097: We will make use of the translation of logic programs
1098: with aggregates to normal logic programs, denoted by $tr$, described
1099: in \cite{PelovDB03}.
1100: The translation in \cite{PelovDB03}
1101: and the unfolding described in the previous subsection
1102: are similar\footnote{It should be noted that our translation
1103: builds on our previous work on semantics of logic
1104: programming with sets and aggregates
1105: \cite{DovierPR01,DovierPR03,ElkabaniPS04}
1106: and was independently developed w.r.t. the work in
1107: \cite{PelovDB03}.}.
1108:
1109: For the sake of completeness, we will review the translation
1110: of \cite{PelovDB03}, presented using the notation of our paper.
1111: Given a ground logic program with aggregates $P$, $tr(P)$ denotes the
1112: ground normal logic program obtained after the translation.
1113: The process begins with the translation of each aggregate atom
1114: $\ell$ of the form $aggr(s) \:\: \texttt{op} \:\: Result$
1115: into a disjunction $tr(\ell) = \bigvee F^{{\cal H}(\ell)}_{(s_1,s_2)}$, where
1116: %$(s_1,s_2)$ belongs to an index set,
1117: $s_1 \subseteq s_2 \subseteq {\cal H}(\ell)$, and
1118: each $F^{{\cal H}(\ell)}_{(s_1,s_2)}$ is a conjunction of the form
1119: %
1120: \[
1121: \bigwedge_{l \in s_1} l \wedge \bigwedge_{l \in {\cal H}(\ell)
1122: \setminus s_2} \naf l
1123: \]
1124: %
1125: The construction of $tr(\ell)$ considers only the pairs $(s_1,s_2)$
1126: that satisfy the following condition:
1127: each interpretation $I$ such that $s_1 \subseteq I$
1128: and ${\cal H}(\ell) \setminus s_2 \cap I = \emptyset$ must satisfy $\ell$.
1129: The translation
1130: $tr(P)$ is then created by replacing rules with disjunction
1131: in the body by a set of standard rules in a straightforward way. For example,
1132: the rule
1133: %
1134: \[
1135: a \leftarrow (b \vee c), d
1136: \]
1137: is replaced by the two rules
1138: %
1139: \[
1140: \begin{array}{lcl}
1141: a \leftarrow b, d & \hspace{1cm} &
1142: a \leftarrow c, d\\
1143: \end{array}
1144: \]
1145: %
1146: From the definitions of $tr(\ell)$ and of aggregate solutions, we have the
1147: following simple lemma:
1148: %
1149: \begin{lemma} \label{tr1}
1150: For every aggregate atom $\ell$ of the form
1151: $aggr(s) \:\: \texttt{op} \:\: Result$,
1152: $S$ is a solution of $\ell$ if and only if
1153: $F^{{\cal H}(\ell)}_{(S\mydot p,{\cal H}(\ell) \setminus S\mydot n)}$
1154: is a disjunct in $tr(\ell)$.
1155: \end{lemma}
1156: %
1157: We next show that fixed point answer sets of $P$ are answer sets of $tr(P)$.
1158:
1159: \begin{lemma}
1160: For a program $P$, $M$ is a fixpoint answer set of $P$
1161: iff $M$ is an answer set of $tr(P)$.
1162: \end{lemma}
1163: %
1164: \begin{proof}
1165: Let $M$ be an interpretation of $P$ and $R = unfolding(P,M)$.
1166: We have that $R$ is a positive program.
1167: Furthermore, let $Q$ denote the result of the Gelfond-Lifschitz reduction of
1168: $tr(P)$ with respect to $M$, i.e., $Q = (tr(P))^M$.
1169: We will prove by induction on $k$
1170: that if $M$ is an answer set of $Q$
1171: then $T_Q \uparrow k = T_R \uparrow k$ for every $k \ge 0$.
1172: The equation holds trivially for $k=0$. Let us consider
1173: now the case for $k$, assuming that $T_Q \uparrow l = T_R \uparrow l$
1174: for $0 \le l < k$.
1175:
1176: \begin{enumerate}
1177: \item Consider $p \in T_Q \uparrow k$.
1178: This means that there exists some rule $r' \in Q$ such that
1179: $head(r') = p$ and $body(r') \subseteq T_Q \uparrow (k-1)$.
1180: $r' \in Q$ if and only if there exists some
1181: $r \in P$ such that $r' \in tr(r)$. Together with Lemma \ref{tr1},
1182: we can conclude that there exists a sequence of aggregate solutions
1183: $\langle S_c \rangle_{c \in agg(r)}$ for the aggregate atoms in $body(r)$
1184: such that $pos(r') = pos(r) \cup \bigcup_{c \in agg(r)} S_c\mydot p$, and
1185: $(neg(r) \cup \bigcup_{c \in agg(r)} S_c\mydot n) \cap M = \emptyset$.
1186: This implies that $r' \in R$. Together with the
1187: inductive hypothesis, we can conclude that $p \in T_R \uparrow k$.
1188:
1189: \item Consider $p \in T_R \uparrow k$. This implies that
1190: there exists some rule $r' \in R$ such that
1191: $head(r') = p$ and $body(r') \subseteq T_R \uparrow (k-1)$. From
1192: the definition of $R$, we conclude
1193: that there exists some rule
1194: $r \in ground(P)$ and a sequence of aggregate solutions
1195: $\langle S_c \rangle_{c \in agg(r)}$ for the aggregate atoms in $body(r)$
1196: such that $pos(r') = pos(r) \cup \bigcup_{c \in agg(r)} S_c\mydot p$, and
1197: $(neg(r) \cup \bigcup_{c \in agg(r)} S_c\mydot n) \cap M = \emptyset$.
1198: Using Lemma \ref{tr1}, we can conclude that $r' \in Q$.
1199: Together with the
1200: inductive hypothesis, we can conclude that $p \in T_Q \uparrow k$.
1201: \end{enumerate}
1202: Similar arguments can be used to show that if $M$ is an answer set of
1203: $R$, $T_Q \uparrow k = T_R \uparrow k$ for every $k \ge 0$, which means
1204: that $M$ is an answer set of $Q$.
1205: \end{proof}
1206:
1207: In \cite{PelovDB03}, it is shown that answer sets of $tr(P)$ coincide
1208: with the \emph{two-valued partial stable models} of $P$ (defined by the
1209: operator $\Phi^{aggr}_P$). This, together with the above lemma
1210: and Theorem \ref{fixpointasp}, allows us to conclude the following
1211: theorem.
1212:
1213: \begin{theorem}
1214: For a program with aggregates $P$, $M$ is an fixpoint answer set of
1215: $P$ if and only if it is a fixpoint of the operator $\Phi^{aggr}_P$
1216: of \cite{PelovDB04}.
1217: \end{theorem}
1218:
1219:
1220:
1221:
1222:
1223: \subsection{Complexity Considerations}
1224:
1225: We will now discuss the complexity of computing
1226: fixpoint answer sets. In what follows, we will assume that
1227: the program $P$ is given and it is a ground program whose language
1228: is finite. By the \emph{size} of a program, we
1229: mean the number of rules and atoms present in it, as in \cite{faberLP04}.
1230: Observe that, in order to support the computation of the iterations
1231: of the $K^P_M$ operator, we need the ability to determine
1232: whether a given $\langle I,J \rangle$ is a solution
1233: of an aggregate atom.
1234: For this reason, we classify programs with aggregates
1235: by the computational complexity of its aggregates.
1236: We define a notion, called $C$-{\em decidability},
1237: where $C$ denotes a complexity class in
1238: the complexity hierarchy, as follows.
1239:
1240: \begin{definition}
1241: Given an aggregate atom $\ell$ and an interpretation $M$,
1242: we say that $\ell$ is $C$-{\em decidable} if
1243: its truth value with respect to $M$ can
1244: be decided by an oracle of the complexity $C$.
1245: A program $P$ is called {\em $C$-decidable} if the aggregate
1246: atoms occurring in $P$ are $C$-decidable.
1247: \end{definition}
1248:
1249: It is easy to see that aggregate atoms built using
1250: the standard aggregate functions
1251: ({\sc Sum, Min, Max, Count, Avg}) and
1252: relations ($=,\ne,\geq,>,\leq,<$) are polynomially
1253: decidable.
1254: The solution checking problem is defined as follows.
1255: %
1256: \begin{definition}
1257: [(SCP) Solution Checking Problem]
1258: {\em\bf Given} an aggregate atom $\ell$, its language
1259: extension ${\cal H}(\ell)$, and a pair of disjoint sets
1260: $I, J \subseteq {\cal H}(\ell)$,
1261: {\em\bf Determine} whether $\langle I,J \rangle$ is a solution of $\ell$.
1262: \end{definition}
1263: %
1264: We have the following lemma.
1265: %
1266: \begin{lemma} \label{l5}
1267: The SCP is in
1268: {\bf co{-}NP}$^C$ for $C$-decidable aggregate atoms.
1269: \end{lemma}
1270: \begin{proof}
1271: We will show that the complexity of the inverse problem of the
1272: SCP is in {\bf NP}$^C$, i.e.,
1273: determining whether
1274: $\langle I, J \rangle$ is not a solution of $\ell$
1275: is in {\bf NP}$^C$.
1276:
1277: By definition,
1278: $\langle I, J \rangle$ is not a solution of $\ell$ if there exists
1279: an interpretation $M$
1280: such that $I \subseteq M$, $J \cap M = \emptyset$,
1281: and $M \not\models \ell$. To answer this question,
1282: we can guess an interpretation $M$
1283: and check whether $\ell$ is false in $M$.
1284: If it is, we conclude that
1285: $\langle I, J \rangle$ is not a solution of $\ell$.
1286: Because $\ell$ is $C$-decidable and there are at most
1287: $2^{|{\cal H}(\ell) \setminus (I \cup J)|}$ interpretations
1288: that can be used in checking whether
1289: $\langle I, J \rangle$ is not a solution of $\ell$,
1290: we conclude that the complexity of the inverse problem is
1291: in {\bf NP}$^C$.
1292: \end{proof}
1293: %
1294: We will now address the problem of answer set checking and
1295: determining the existence of answer set.
1296: %
1297: \begin{definition}
1298: [(ACP) Answer Set Checking Problem]
1299: {\em\bf Given} an interpretation $M$ of $P$,
1300: {\em\bf Determine} whether $M$ is an answer set of $P$.
1301: \end{definition}
1302: %
1303: %
1304: \begin{definition}
1305: [(AEP) Answer Set Existence Problem]
1306: {\em\bf Given} a program $P$,
1307: {\em\bf Determine} whether $P$ has a fixpoint answer set.
1308: \end{definition}
1309: %
1310: The following theorem follows from Lemma \ref{l5}.
1311: %
1312: \begin{theorem}
1313: The ACP of $C$-decidable programs is in
1314: {\bf co{-}NP}$^C$.
1315: \end{theorem}
1316: \begin{proof}
1317: The main tasks in checking whether $M$ is an answer set of $P$ are {\em (i)}
1318: computing $^M\!P$; and {\em (ii)} computing $lfp(K_M^P)$.
1319: Obviously, $^M\!P$ can be constructed in time linear in the size of $P$,
1320: since the reduction relies on the
1321: satisfiability test of a negation-as-failure
1322: literal $\ell$ w.r.t. $M$.
1323: Computing $lfp(K_M^P)$ requires at most $na$ iterations,
1324: i.e., $lfp(K_M^P) = K_M^P \uparrow na$,
1325: where $na$ is the number of atoms of $P$, each step
1326: is in {\bf co{-}NP}$^C$, due to the requirement of solution
1327: checking.
1328: \end{proof}
1329: %
1330: This theorem allows us to conclude the following result.
1331: \begin{corollary}
1332: The AEP for $C$-decidable program
1333: is in {\bf NP}$^{\textnormal{\bf co{-}NP}^C}$.
1334: \end{corollary}
1335: %
1336: So far, we discussed the worst case analysis of answer set
1337: checking and determining the existing of an answer set based on
1338: a general assumption about the complexity of computing the aggregate functions
1339: and checking the truth value of aggregate atoms.
1340: Next we analyze the complexity of these problems
1341: w.r.t. the class of programs whose aggregate atoms
1342: are built using standard
1343: aggregate functions and operators.
1344:
1345: \subsubsection{Complexity of Solution Checking for Standard Aggregates}
1346:
1347: We will now focus on the class of programs
1348: defined in Section \ref{sec2} with standard aggregate
1349: functions ({\sc Sum, Min, Max, Count, Avg}) and relations
1350: ($=$, $\geq$, $>$, $\leq$, $<$, $\ne$). It is easy to see that all
1351: aggregate atoms involving these functions and relations
1352: are {\bf P}-decidable. Therefore,
1353: by Lemma \ref{l5}, the SCP for standard aggregates will be at
1354: most {\bf co{-}NP}. We will now show that
1355: it is {\bf co{-}NP}-complete.
1356:
1357: \begin{theorem} \label{t10}
1358: The SCP for standard aggregates is
1359: {\bf co{-}NP}-complete.
1360: \end{theorem}
1361: \begin{proof}
1362: Membership follows from Lemma \ref{l5}.
1363: To prove hardness, we will translate
1364: a well-known {\bf NP}-complete problem,
1365: namely the subset sum problem \cite{cormen},
1366: to the complement of the solution checking problem.
1367: An instance $Q$ of the subset sum problem is given
1368: by a set of non-negative integers $S$ and an
1369: integer $t$, and the question is to determine whether
1370: there exists any non-empty subset $A$ of
1371: $S$ such that $\sum_{x \in A} x = t$.
1372:
1373: Let ${\cal H}(\ell) = \{p(x) \mid x \in S\}$ for some unary predicate $p$.
1374: We define an instance of the solution checking problem,
1375: $s(Q)$, by setting $I=\emptyset$, $J=\emptyset$, and
1376: $\ell = \textnormal{\sc Sum}(\{X \mid p(X)\}) \ne t$. It is easy to see
1377: that $s(Q)$ is equivalent to $Q$ as follows:
1378: if $\langle I,J \rangle$ is a solution of $\ell$ then $Q$
1379: does not have an answer;
1380: if $\langle I,J \rangle$ is not a solution to $\ell$ then
1381: $Q$ has an answer. This proves the desired result.
1382: \end{proof}
1383:
1384: The above theorem shows that, in general, the inclusion of
1385: standard aggregates implies that the answer set checking problem and
1386: the problem of determining the existing of an answer set are
1387: in {\bf co{-}NP} and {\bf NP}$^{\textnormal{\bf co{-}NP}}$ respectively.
1388: Fortunately, there is a large class of programs with
1389: standard aggregates for which the complexity of these two
1390: problems are in {\bf P} and {\bf NP} respectively, as shown
1391: next.
1392:
1393: \begin{lemma} \label{l10}
1394: Let $\ell$ be an aggregate of the form
1395: $\textnormal{\sc Sum}(\{X \mid p(X)\}) = v$, where $v$ is a constant
1396: in $\mathbf{R}$.
1397: Let $I,J \subseteq {\cal H}(\ell)$ such that $I \cap J = \emptyset$.
1398: Then,
1399: determining whether $\langle I, J \rangle$ is a solution of $\ell$
1400: can be done in time polynomial in the size of ${\cal H}(\ell)$.
1401: \end{lemma}
1402: \begin{proof}
1403: Let us denote with $\pi$ the function that projects an element $p$
1404: of ${\cal H}(\ell)$ to the value that $p$ assigns to the collected
1405: variable. This value will be denoted by $\pi(p)$. We prove the lemma
1406: by providing a polynomial algorithm for determining whether
1407: $\langle I, J \rangle$ is a solution of $\ell$.
1408: %
1409: \begin{center}
1410: \begin{minipage}[t]{.8\textwidth}
1411: {\begin{tabbing}
1412: iiii\=iiii\=iiiii\=iiii\=iiii\=iiii\=iiii\=iiii\=iiii\kill
1413: 1:\>{\bf function} {\tt Check\_Solution} ($v$, $\langle I, J\rangle$,
1414: ${\cal H}(\ell)$)\\
1415: 2:\>\> compute $s = \Sigma_{p \in I} \pi(p)$ \\
1416: 3:\>\> {\bf if} $s \ne v$ {\bf then return false}\\
1417: 4:\>\> {\bf if} ${\cal H}(\ell) \setminus (I \cup J) = \emptyset$
1418: {\bf then return true};\\
1419: 5:\>\> {\bf forall} ($p \in {\cal H}(\ell) \setminus (I \cup J)$)\\
1420: 6:\>\>\> {\bf if} $\pi(p) \ne 0$ {\bf then return false} \\
1421: 7:\>\> {\bf endfor} \\
1422: 8:\>\> {\bf return true} \\
1423: \end{tabbing}}
1424: \end{minipage}
1425: \end{center}
1426: It is easy to see that the above algorithm returns true (resp.
1427: false) if and only if
1428: $\langle I, J \rangle$ is (resp. is not) a solution of $\ell$.
1429: Furthermore, the time complexity of the above algorithm
1430: is polynomial in the size of ${\cal H}(\ell)$. This proves the lemma.
1431: \end{proof}
1432:
1433: The above lemma shows that the solution checking problem can be
1434: solved in polynomial time for a special type of standard aggregate
1435: atoms. Indeed, this can be proven for all standard aggregates but those
1436: of the form $\textnormal{\sc Sum} \ne v$ and
1437: $\textnormal{\sc Avg} \ne v$.
1438:
1439: \begin{lemma}
1440: Let $\ell$ be the aggregate $agg(s) \;\mathbf{ op }\; v$
1441: where $agg \not\in \{\textnormal{\sc Sum, Avg}\}$
1442: or $agg \in \{\textnormal{\sc Sum, Avg}\}$ and
1443: $\mathbf{op}$ is not `$\ne$'.
1444: Let $I, J \subseteq {\cal H}(\ell)$, $I \cap J = \emptyset$, and
1445: $v \in \mathbf{R}$.
1446: Then, checking if
1447: $\langle I, J \rangle$ is a solution of $\ell$ can be done
1448: in time polynomial in the size of ${\cal H}(\ell)$.
1449: \end{lemma}
1450: \begin{proof}
1451: The proof can be done similarly to the proof of Lemma \ref{l10}:
1452: for each type of atom, we develop an algorithm, which
1453: returns true (resp. false) if $\langle I,J\rangle$
1454: is (resp. is not) a solution of $\ell$.
1455: For brevity, we only discuss the steps which need to be done.
1456: It should be noted that each of these steps can
1457: be done in polynomial time in the size of ${\cal H}(\ell)$,
1458: which implies the conclusion of the lemma.
1459:
1460: \begin{itemize}
1461:
1462: \item {\sc Sum:} Let $s = \sum_{p\in I} \pi(p)$. All cases can
1463: be handled in time $O(|{\cal H}(\ell)|)$. Let us consider
1464: the various cases for {\bf op}.
1465:
1466: \begin{list}{$\bullet$}{\topsep=1pt \parsep=0pt \itemsep=1pt}
1467: \item The case {\bf op} is '=' has been discussed in Lemma \ref{l10}.
1468:
1469: \item For ${\bf op} \in\{\geq, >\}$,
1470: let $H_1 = \{p \mid p \in {\cal H}(\ell)
1471: \setminus (I \cup J),\; \pi(p)<0\}$.
1472: We have that
1473: $\langle I,J \rangle$ is a solution of $\ell$ if and only if
1474: $s \; \mathbf{op} \; v$ and $\sum_{p \in H_1} \pi(p) + s \; \mathbf{op} \; v$.
1475:
1476: \item For $\mathbf{op} \in \{\leq,<\}$, let
1477: $H_1 = \{p \mid p \in {\cal H}(\ell)
1478: \setminus (I \cup J),\; \pi(p)>0\}$.
1479: We have that
1480: $\langle I,J \rangle$ is a solution of $\ell$ if and only if
1481: $s \; \mathbf{op} \; v$ and
1482: $\sum_{p \in H_1} \pi(p) + s \; \mathbf{op} \; v$.
1483: \end{list}
1484:
1485:
1486: \item{\sc Count:} Let $c = |I|$ and
1487: $H_1 = {\cal H}(\ell) \setminus (I \cup J)$. All cases can be
1488: handled in time $O(|{\cal H}(\ell)|)$.
1489:
1490: \begin{list}{$\bullet$}{\topsep=1pt \parsep=0pt \itemsep=1pt}
1491: \item If $\mathbf{op} \in \{>,\ge\}$, then
1492: $\langle I, J\rangle$ is a solution of $\ell$ if and only if
1493: $c \; \mathbf{op} \; v$.
1494:
1495: \item If $\mathbf{op} \in \{=,<,\le\}$, then
1496: $\langle I, J\rangle$ is a solution of $\ell$ if and only if
1497: $c \; \mathbf{op} \; v$
1498: and $c + |H_1| \; \mathbf{op} \; v$.
1499:
1500: \item If $\mathbf{op}$ is $\ne$, then
1501: $\langle I, J\rangle$ is a solution of $\ell$ if and only if
1502: either {\em (i)} $|I| > v$; or
1503: {\em (ii)} $|I| < v$ and $|H_1| < v-|I|$.
1504: \end{list}
1505:
1506:
1507: \item{\sc Min:} Let $c = \min \{\pi(p) \mid p \in I\}$ and
1508: $c_1 = \min \{\pi(p) \mid p \in {\cal H}(\ell) \setminus (I \cup J)\}$.
1509: All cases can be
1510: handled in time $O(|{\cal H}(\ell)|)$.
1511:
1512: \begin{list}{$\bullet$}{\topsep=1pt \parsep=0pt \itemsep=1pt}
1513: \item If $\mathbf{op}$ is $=$ then
1514: we have that
1515: $\langle I,J \rangle$ is a solution of $\ell$ if and only if
1516: $c = v $ and $c_1 \ge v$.
1517:
1518: \item If $\mathbf{op} \in \{\leq,<\}$ then
1519: $\langle I,J \rangle$ is a solution of $\ell$ if and only if
1520: $c \; \mathbf{op} \; v $.
1521:
1522: \item If $\mathbf{op} \in \{\geq,>\}$ then
1523: $\langle I,J \rangle$ is a solution of $\ell$ if and only if
1524: $c \; \mathbf{op} \; v$ and
1525: $c_1 \; \mathbf{op} \; v$.
1526:
1527: \item If $\mathbf{op}$ is $\ne$ then
1528: $\langle I,J \rangle$ is a solution of $\ell$ if and only if
1529: either {\em (i)} $c < v$; or
1530: {\em (ii)} $c > v$ and for every $p \in H_1$,
1531: $\pi(p) \ne v$.
1532: \end{list}
1533:
1534:
1535: \item{\sc Max:}
1536: Let $c = \max \{\pi(p) \mid p \in I\}$ and
1537: $c_1 = \max \{\pi(p) \mid p \in {\cal H}(\ell) \setminus (I \cup J)\}$.
1538: All cases can be
1539: handled in time $O(|{\cal H}(\ell)|)$.
1540:
1541: \begin{list}{$\bullet$}{\topsep=1pt \parsep=0pt \itemsep=1pt}
1542: \item If $\mathbf{op}$ is $=$ then
1543: $\langle I,J \rangle$ is a solution of $\ell$ if and only if
1544: $c = v $ and $c_1 \le v$.
1545:
1546: \item If $\mathbf{op} \in \{\geq,>\}$ then
1547: $\langle I,J \rangle$ is a solution of $\ell$ if and only if
1548: $c \; \mathbf{op} \; v $.
1549:
1550: \item If $\mathbf{op} \in \{\leq,<\}$ then
1551: $\langle I,J \rangle$ is a solution of $\ell$ if and only if
1552: $c \; \mathbf{op} \; v$ and
1553: $c_1 \; \mathbf{op} \; v$.
1554:
1555: \item If $\mathbf{op}$ is $\ne$ then
1556: $\langle I,J \rangle$ is a solution of $\ell$ if and only if
1557: either {\em (i)} $c > v$; or
1558: {\em (ii)} $c < v$ and for every $p \in H_1$,
1559: $\pi(p) \ne v$.
1560: \end{list}
1561:
1562:
1563: \item{\sc Avg:}
1564: Let $a = \frac{\sum_{p\in I} \{\pi(p)\}}{|I|}$
1565: and $H_1 = {\cal H}(\ell)\setminus (I\cup J)$.
1566:
1567: \begin{list}{$\bullet$}{\topsep=1pt \parsep=0pt \itemsep=1pt}
1568: \item If $\mathbf{op}$ is $=$ then
1569: $\langle I,J\rangle$ is a solution of $\ell$ if and only if
1570: $a = v$ and for every $p \in H_1$, $\pi(p) = v$. This can be done
1571: in time $O(|{\cal H}(\ell)|)$.
1572:
1573: \item If $\mathbf{op} \in \{\geq,>\}$ then
1574: let $e_1,\dots, e_r$ be an enumeration of $H_1$
1575: such that $\pi(e_i) \leq \pi(e_{i+1})$ for $1 \leq i\leq r-1$.
1576: $\langle I,J\rangle$ is a solution of $\ell$ if and only if
1577: $a \;\mathbf{op}\; v$ and
1578: for each $ 0 \leq h \leq r$,
1579: \[\sum_{p\in I}\pi(p) + \sum_{i=1}^h \pi(e_i) \;\mathbf{op}\; v\cdot |I|+ v \cdot h.\]
1580: This can be accomplished in time $O(|{\cal H}(\ell)|^2)$.
1581:
1582:
1583: \item If $\mathbf{op} \in \{\leq, <\}$ then
1584: let $e_1,\dots, e_r$ be an enumeration of $H_1$
1585: such that $\pi(e_i) \geq \pi(e_{i+1})$ for $1 \leq i\leq r-1$.
1586: $\langle I,J\rangle$ is a solution of $\ell$ if and only if
1587: $a \;\mathbf{op}\; v$ and
1588: for each $ 0 \leq h \leq r$,
1589: \[ \sum_{p\in I}\pi(p) + \sum_{i=1}^h \pi(e_i) \; \mathbf{op} \; v\cdot |I|+ v \cdot h. \]
1590: This can be accomplished in time $O(|{\cal H}(\ell)|^2)$.
1591: \end{list}
1592: \end{itemize}
1593: \end{proof}
1594: %
1595: The above lemma shows that there is a large class of programs
1596: with aggregates for which the problem of checking an answer set
1597: and the problem of determining the existence of an answer set
1598: belongs to the class {\bf P} and {\bf NP} respectively.
1599:
1600: Observe that similar results can be extrapolated from the discussion
1601: in Pelov's doctoral dissertation~\cite{Pelov04}.
1602:
1603: \section{Conclusions and Future Work}
1604:
1605: In this technical note, we defined $K^P_M$, a fixpoint operator for
1606: verifying answer sets of programs with aggregates. We showed that
1607: the semantics for programs with aggregates described by this operator
1608: provides a new characterization of
1609: the semantics of \cite{SonPE05}
1610: for logic programs with aggregates. This operator converges to the
1611: same semantics as in \cite{Pelov04} when ultimate approximating
1612: aggregates are used.
1613: We also related this semantics to recently proposed semantics
1614: for aggregate programs. We discussed the complexity of the
1615: answer set checking problem and the problem of determining the existence
1616: of an answer set. We showed that, for the class of programs with
1617: standard aggregates without the relation $\ne$ for {\sc Sum} and {\sc Avg},
1618: the complexity of these two problems remains unchanged comparing
1619: to that of normal logic programs. In the future, we would like to
1620: use this idea in an efficient implementation of answer set solvers
1621: with aggregates.
1622:
1623:
1624: \subsubsection*{Acknowledgments}
1625: The authors wish to thank the anonymous
1626: reviewers for their insightful comments and for pointing out
1627: relationships with existing literature, and Dr. Hing Leung for his
1628: suggestions.
1629:
1630: The research has been partially supported by NSF grants
1631: HRD-0420407, CNS-0454066, and CNS-0220590.
1632:
1633: \bibliographystyle{acmtrans}
1634:
1635: \begin{thebibliography}{}
1636:
1637: \bibitem[\protect\citeauthoryear{Cormen et al.}{Cormen et al.}{2001}]{cormen}
1638: {\sc Cormen, T.H., Leiserson, C.E., Rivest, R.L.} {\sc and} {\sc Stein, C.} 2001.
1639: \newblock {\em {Introduction to Algorithms, 2nd Edition}}.
1640: \newblock MIT Press, Cambridge, MA.
1641:
1642: \bibitem[\protect\citeauthoryear{Dovier, Pontelli, and Rossi}{Dovier
1643: et~al\mbox{.}}{2001}]{DovierPR01}
1644: {\sc Dovier, A.}, {\sc Pontelli, E.}, {\sc and} {\sc Rossi, G.} 2001.
1645: \newblock Constructive negation and constraint logic programming with sets.
1646: \newblock {\em New Generation Comput.\/}~{\em 19,\/}~3, 209--256.
1647:
1648: \bibitem[\protect\citeauthoryear{Dovier, Pontelli, and Rossi}{Dovier
1649: et~al\mbox{.}}{2003}]{DovierPR03}
1650: {\sc Dovier, A.}, {\sc Pontelli, E.}, {\sc and} {\sc Rossi, G.} 2003.
1651: \newblock Intensional Sets in CLP.
1652: \newblock In {\em International Conference on Logic Programming},
1653: Springer, 284--299.
1654:
1655: \bibitem[\protect\citeauthoryear{Elkabani, Pontelli, and Son}{Elkabani
1656: et~al\mbox{.}}{2004}]{ElkabaniPS04}
1657: {\sc Elkabani, I.}, {\sc Pontelli, E.}, {\sc and} {\sc Son, T.~C.} 2004.
1658: \newblock Smodels with CLP and its Applications: a Simple and Effective
1659: Approach to Aggregates in ASP.
1660: \newblock In {\em International Conference on Logic Programming},
1661: Springer, 73--89.
1662:
1663: \bibitem[\protect\citeauthoryear{Faber, Leone, and Pfeifer}{Faber
1664: et~al\mbox{.}}{2004}]{faberLP04}
1665: {\sc Faber, W.}, {\sc Leone, N.}, {\sc and} {\sc Pfeifer, G.} 2004.
1666: \newblock Recursive Aggregates in Disjunctive Logic Programs: Semantics and
1667: Complexity.
1668: \newblock In {\em JELIA}, Springer, 200--212.
1669:
1670:
1671: \bibitem[\protect\citeauthoryear{Gelfond}{Gelfond}{2002}]{a-prolog}
1672: {\sc Gelfond, M.} 2002.
1673: \newblock {Representing Knowledge in A-Prolog}.
1674: \newblock In {\em Computational Logic: Logic Programming and Beyond},
1675: Springer Verlag, 413--451.
1676:
1677: \bibitem[\protect\citeauthoryear{Gelfond and Lifschitz}{Gelfond and
1678: Lifschitz}{1988}]{GL88}
1679: {\sc Gelfond, M.} {\sc and} {\sc Lifschitz, V.} 1988.
1680: \newblock The Stable Model Semantics for Logic Programming.
1681: \newblock In {\em International
1682: Conf.~and Symp. on Logic Programming}, MIT Press, 1070--1080.
1683:
1684: \bibitem[\protect\citeauthoryear{Kemp and Stuckey}{Kemp and
1685: Stuckey}{1991}]{KempS91}
1686: {\sc Kemp, D.~B.} {\sc and} {\sc Stuckey, P.~J.} 1991.
1687: \newblock Semantics of Logic Programs with Aggregates.
1688: \newblock In {\em ISLP}, MIT Press, 387--401.
1689:
1690: \bibitem[\protect\citeauthoryear{Lloyd}{Lloyd}{1987}]{lloyd}
1691: {\sc Lloyd, J.} 1987.
1692: \newblock \emph{Foundations of Logic Programming}.
1693: \newblock Springer Verlag.
1694:
1695: \bibitem[\protect\citeauthoryear{Mumick, Pirahesh, and Ramakrishnan}{Mumick
1696: et~al\mbox{.}}{1990}]{MumickPR90}
1697: {\sc Mumick, I.~S.}, {\sc Pirahesh, H.}, {\sc and} {\sc Ramakrishnan, R.} 1990.
1698: \newblock The Magic of Duplicates and Aggregates.
1699: \newblock In {\em Int. Conf. on Very Large Data Bases},
1700: Morgan Kaufmann,
1701: 264--277.
1702:
1703: \bibitem[\protect\citeauthoryear{Pelov}{Pelov}{2004}]{Pelov04}
1704: {\sc Pelov, N.} 2004.
1705: \newblock {Semantic of Logic Programs with Aggregates}.
1706: \newblock Ph.D. thesis, Katholieke Universiteit Leuven.
1707:
1708:
1709: \bibitem[\protect\citeauthoryear{Pelov, Denecker, and Bruynooghe}{Pelov
1710: et~al\mbox{.}}{2003}]{PelovDB03}
1711: {\sc Pelov, N.}, {\sc Denecker, M.}, {\sc and} {\sc Bruynooghe, M.} 2003.
1712: \newblock {Translation of Aggregate Programs to Normal Logic Programs}.
1713: \newblock In {\em {ASP: Advances in Theory and
1714: Implementation}}, CEUR Workshop Proceedings. {29--42}.
1715:
1716: \bibitem[\protect\citeauthoryear{Pelov, Denecker, and Bruynooghe}{Pelov
1717: et~al\mbox{.}}{2004}]{PelovDB04}
1718: {\sc Pelov, N.}, {\sc Denecker, M.}, {\sc and} {\sc Bruynooghe, M.} 2004.
1719: \newblock Partial Stable Models for Logic Programs with Aggregates.
1720: \newblock In {\em LPNMR},
1721: Springer,
1722: 207--219.
1723:
1724: \bibitem[\protect\citeauthoryear{Ross and Sagiv}{Ross and
1725: Sagiv}{1997}]{RossS97}
1726: {\sc Ross, K.~A.} {\sc and} {\sc Sagiv, Y.} 1997.
1727: \newblock Monotonic Aggregation in Deductive Database.
1728: \newblock {\em J. Comput. Syst. Sci.\/}~{\em 54,\/}~1, 79--97.
1729:
1730: \bibitem[\protect\citeauthoryear{Son, Pontelli, and Elkabani}{Son
1731: et~al\mbox{.}}{2005}]{SonPE05}
1732: {\sc Son, T.~C.}, {\sc Pontelli, E.}, {\sc and} {\sc Elkabani, I.} 2005.
1733: \newblock {A Translational Semantics for Aggregates in Logic Programming }.
1734: \newblock Tech. Rep. {CS-2005-006}, New Mexico State University.
1735: \newblock \url{www.cs.nmsu.edu/CSWS/php/techReports.php?rpt_year=2005}.
1736:
1737: \bibitem[\protect\citeauthoryear{Zaniolo, Arni, and Ong}{Zaniolo
1738: et~al\mbox{.}}{1993}]{ZanioloAO93}
1739: {\sc Zaniolo, C.}, {\sc Arni, N.}, {\sc and} {\sc Ong, K.} 1993.
1740: \newblock Negation and Aggregates in Recursive Rules: the LDL++ Approach.
1741: \newblock In {\em DOOD}. 204--221.
1742:
1743: \end{thebibliography}
1744:
1745: %\newpage
1746: \section*{Appendix A --- Correspondence between $K_M^P$ and $\Phi^{aggr}_P$}
1747:
1748: We assume that
1749: the readers are familiar with the notations and definitions
1750: introduced in \cite{PelovDB04}.
1751:
1752: The three-valued immediate consequence operator
1753: $\Phi_P^{aggr}$ of a program $P$ in \cite{PelovDB04},
1754: maps 3-valued interpretations to 3-valued interpretations. But
1755: 3-valued interpretations can be split up in pairs $(I, J)$
1756: of two valued interpretations such that $I \subseteq J$.
1757: Hence, an operator $\Phi_P^{aggr}$ can be viewed as an operator
1758: from pairs $(I,J)$ to pairs $\Phi_P^{aggr}(I,J) = (I',J')$
1759: of 2-valued interpretations. It follows
1760: that $\Phi_P^{aggr}$ determines two component operators
1761: $\Phi_P^{aggr,1} (I, J) = I'$ and
1762: $\Phi_P^{aggr,2} (I, J) = J'$. The correspondence between
1763: $K_M^P$ and $\Phi^{aggr}_P$ is shown in the following claim.
1764:
1765: \medskip \noindent
1766: {\bf Claim.} For every $I \subseteq M$,
1767: $K_M^P(I) = \Phi^{aggr,1}_P(I,M)$.
1768:
1769: \begin{proof}
1770: First, let us identify the aggregate atoms
1771: $agg(s) \;\; \mathbf{op} \;\; v$
1772: in this paper with aggregate atoms $R(s, v)$
1773: of \cite{PelovDB04}. E.g., {\sc Max}$(s) = v$
1774: corresponds to {\sc Max}$(s, v)$; {\sc Max}$(s) \le v$
1775: corresponds to {\sc Max}$_\le (s, v)$.
1776: Now we compare the definition of $K_M^P$ and $\Phi^{aggr,1}_P$
1777: in the case that $I \subseteq M$.
1778: For simplicity let us assume that atom $a$ is defined by only one
1779: ground rule, say $r$.
1780:
1781: $a \in K_M^P(I)$ iff $pos(r)$ is true in $I$,
1782: $neg(r)$ is false in $M$, and for each $\ell \in aggr(r)$,
1783: $l$ has a solution
1784: $(I \cap M \cap {\cal H}(\ell), {\cal H}(\ell) \setminus M)$.
1785:
1786: $a \in \Phi^{aggr,1}_P(I,M)$ iff $pos(r)$ is true in $I$,
1787: $neg(r)$ is false in $M$, and for each $\ell \in aggr(r)$,
1788: $l$ evaluates to true, i.e., if
1789: $U^1_R(s^{(I,M)})) = t$. Here, $U^1_R$ is the first component of
1790: the three-valued aggregate, and $s^{(I,M)}$ is the
1791: evaluation of the set expression under the 3-valued interpretation
1792: $(I,M)$.
1793:
1794: All that remains to be done is to show that
1795: $(I \cap M \cap {\cal H}(\ell), {\cal H}(\ell) \setminus M)$ is a
1796: solution for $l$ iff $U^1_R(s^{(I,M)}) = t$.
1797: Recall that we are considering the case where
1798: $I \subseteq M$, therefore the first expression simplifies to
1799: $(I \cap {\cal H}(\ell), {\cal H}(\ell) \setminus M)$.
1800:
1801: Let us focus on set aggregates but the argument for multisets
1802: is the same. Let us consider an aggregate atom
1803: $$\ell = agg(s)\;\; \mathbf{op} \;\;v$$
1804: where $$s = \{X \mid p(d_1,\ldots,d_{i-1},X, d_{i+1},\ldots,d_n)\}$$
1805: and $X$ is the only variable and
1806: $d_1,\ldots,d_n$ are members of the Herbrand universe.
1807: For any $I \subseteq M$, \\
1808: \begin{center}
1809: $(I \cap {\cal H}(\ell), {\cal H}(\ell) \setminus M)$
1810: is a solution for $\ell$ \\
1811: iff for each $J$ such
1812: that
1813: $I \cap {\cal H}(\ell) \subseteq J$ and
1814: $J \cap ({\cal H}(\ell) \setminus M) = \emptyset$,
1815: $J \models \ell$ \\
1816: iff for each $J$ such that $I \subseteq J \subseteq M$,
1817: $J \models \ell$.
1818: \end{center}
1819: The latter equivalence is perhaps not entirely trivial
1820: but it follows easily from the fact that $J \models \ell \Leftrightarrow
1821: J'\models \ell$ whenever $J \cap {\cal H}(\ell) = J' \cap {\cal H}(\ell)$.
1822:
1823: In \cite{PelovDB04}, the value $s^{(I,M)}$
1824: is a three-valued (multi-)set, which can be written as a pair of
1825: two valued sets $(S_1, S_2)$ where
1826: $$S_1 = \{d \mid I \models p(d_1,\ldots,d_{i-1},d,d_{i+1},\ldots,d_n)\}$$
1827: and
1828: $$S_2 = \{d \mid M \models p(d_1,\ldots,d_{i-1},d,d_{i+1},\ldots,d_n)\}.$$
1829:
1830: By definition of $U^1_R$,
1831: $U^1_R(s^{(I,M)})) = t$ iff for each set $S$ such that
1832: $S_1 \subseteq S \subseteq S_2$, $R(S, v)$ is true.
1833: It is straightforward to see that the conditions in this paragraph
1834: and the previous one are equivalent.
1835: \end{proof}
1836:
1837: \end{document}
1838:
1839: