1: % -----------------------------------------------------------------------------
2: %
3: % This file contains all the latex sources for
4: % an extended version of the paper
5: %
6: % ``Unfolding Partiality and Disjunctions in Stable Model Semantics''
7: % by Janhunen, T., Niemelä, I., Simons, P., and You, J.
8: %
9: % presented at KR'2000.
10: %
11: % The only external files needed: experiment-*-vs-*-*.ps (PostScript files)
12: %
13:
14: \documentclass[12pt]{article}
15:
16: \usepackage[T1]{fontenc}
17: \usepackage{latexsym}
18: \usepackage{graphicx}
19: \usepackage{amsmath}
20: \usepackage{theorem}
21: \usepackage{epsfig}
22: \usepackage{url}
23:
24: %------------------------------------------------------------------------------
25: % Environments and such
26:
27: \newtheorem{theorem}{Theorem}[section]
28: \newtheorem{corollary}[theorem]{Corollary}
29: \newtheorem{definition}[theorem]{Definition}
30: \newtheorem{proposition}[theorem]{Proposition}
31: \newtheorem{lemma}[theorem]{Lemma}
32:
33: \theorembodyfont{\rm}
34: \newtheorem{example}[theorem]{Example}
35: \newtheorem{remark}[theorem]{Remark}
36:
37: \newcommand{\ebox}{\mbox{}\nobreak\hfill\hspace{6pt}$\Box$}
38:
39: \newenvironment{proof}[0]{\noindent\textbf{PROOF.}}{\ebox}
40:
41: %------------------------------------------------------------------------------
42: % Notation of the paper
43:
44: \DeclareMathSymbol{\naf}{\mathord}{symbols}{"18}
45:
46: % Sets
47:
48: \newcommand{\union}{\cup}
49: \newcommand{\Union}{\bigcup}
50: \newcommand{\isect}{\cap}
51: \newcommand{\pair}[2]{\langle{#1},{#2}\rangle}
52: \newcommand{\rg}[3]{#1#2\dots#2#3}
53: \newcommand{\set}[1]{\{{#1}\}}
54: \newcommand{\eset}[2]{\{{#1},\ldots,{#2}\}}
55: \newcommand{\sel}[2]{\{{#1}\,|\,{#2}\}}
56: \newcommand{\func}[3]{{#1}:{#2}\rightarrow{#3}}
57:
58: % Logic
59:
60: \newcommand{\true}{\mathbf{t}}
61: \newcommand{\false}{\mathbf{f}}
62: \newcommand{\undef}{\mathbf{u}}
63: \newcommand{\True}[1]{{#1}^{\true}}
64: \newcommand{\False}[1]{{#1}^{\false}}
65: \newcommand{\Undef}[1]{{#1}^{\undef}}
66: \newcommand{\Lor}[1]{\bigvee{#1}}
67: \newcommand{\val}[2]{{#1}({#2})}
68:
69: % Programs
70:
71: \newcommand{\hb}[1]{\mathrm{Hb}(#1)}
72: \newcommand{\at}[1]{\mathsf{#1}}
73: \newcommand{\IF}{\leftarrow}
74: \newcommand{\END}{;\;\;}
75: \newcommand{\pot}[1]{{#1}^{\bullet}}
76: \newcommand{\GLred}[2]{{#1}^{#2}}
77: \newcommand{\red}[2]{{#1}_{#2}}
78:
79: \newcommand{\UFi}{UF1}
80: \newcommand{\UFii}{UF2}
81: \newcommand{\UFiii}{UF3}
82:
83: \newcommand{\sys}[1]{\textsc{#1}}
84:
85: \newcommand{\nlp}[1]{#1_\mathrm{N}}
86: \newcommand{\dlp}[1]{#1_\mathrm{D}}
87: \newcommand{\heads}[1]{\mathrm{Heads}(#1)}
88:
89: % Translations
90:
91: \newcommand{\tr}[2]{\mathrm{Tr}_{\mathrm{#1}}(#2)}
92: \newcommand{\trop}[1]{\mathrm{Tr}_{\mathrm{#1}}}
93:
94: \newcommand{\genO}[1]{{\mathrm{G0}}(#1)}
95: \newcommand{\genI}[1]{{\mathrm{G1}}(#1)}
96: \newcommand{\support}[1]{{\mathrm{Supp}}(#1)}
97: \newcommand{\supp}[1]{{#1^{\mathrm{s}}}}
98:
99: \newcommand{\gen}[1]{{\mathrm{Gen}}(#1)}
100: \newcommand{\test}[2]{{\mathrm{Test}}(#1,#2)}
101:
102: \newcommand{\expand}{\mathit{expand}}
103: \newcommand{\extend}{\mathit{extend}}
104: \newcommand{\smodels}{\mathit{smodels}}
105: \newcommand{\gnt}{\mathit{gnt}}
106: \newcommand{\conflict}{\mathit{conflict}}
107: \newcommand{\heuristic}{\mathit{heuristic}}
108: \newcommand{\isminimal}{\mathit{minimal}}
109: \newcommand{\keyw}[1]{\textbf{#1}}
110: \newcommand{\GP}{G}
111:
112: % Complexity classes
113:
114: \newcommand{\NP}{\mathrm{NP}}
115:
116: %------------------------------------------------------------------------------
117:
118: \begin{document}
119:
120: \title{\vspace{-1\baselineskip}\
121: Unfolding Partiality and Disjunctions \\
122: in Stable Model Semantics\thanks{\
123: A preliminary version of this paper \cite{JNSY00:kr} appears in
124: the Proceedings of the 7th International Conference on
125: the Principles of Knowledge Representation and Reasoning,
126: KR'2000.}}
127:
128: \normalsize
129: \author{
130: Tomi Janhunen and Ilkka Niemelä \\
131: Department of Computer Science and Engineering \\
132: Helsinki University of Technology \\
133: P.O.Box 5400, FIN-02015 HUT, Finland \\
134: \{Tomi.Janhunen,Ilkka.Niemela\}@hut.fi \\
135: \ \\
136: Dietmar Seipel \\
137: University of Würzburg \\
138: Am Hubland, D-97074 Würzburg, Germany \\
139: seipel@informatik.uni-wuerzburg.de \\
140: \ \\
141: Patrik Simons \\
142: Neotide Oy \\
143: Wolffintie 36 \\
144: FIN-65200 Vaasa, Finland \\
145: Patrik.Simons@neotide.fi \\
146: \ \\
147: Jia-Huai You \\
148: Department of Computing Science \\
149: University of Alberta \\
150: Edmonton, Alberta, Canada T6G 2H1\\
151: you@cs.ualberta.ca
152: }
153: \date{}
154:
155: \maketitle
156:
157: \begin{abstract}
158: The paper studies an implementation methodology for partial and
159: disjunctive stable models where partiality and disjunctions are
160: unfolded from a logic program so that an implementation of stable
161: models for normal (disjunction-free) programs can be used as the core
162: inference engine. The unfolding is done in two separate steps.
163: Firstly, it is shown that partial stable models can be captured by
164: total stable models using a simple linear and modular program
165: transformation. Hence, reasoning tasks concerning partial stable models can
166: be solved using an implementation of total stable models. Disjunctive
167: partial stable models have been lacking implementations which now
168: become available as the translation handles also the disjunctive case.
169: Secondly, it is shown how total stable models of disjunctive programs
170: can be determined by computing stable models for normal programs.
171: Hence, an implementation of stable models of normal programs can be
172: used as a core engine for implementing disjunctive programs. The
173: feasibility of the approach is demonstrated by constructing a system
174: for computing stable models of disjunctive programs using the
175: \sys{smodels} system as the core engine. The performance of the resulting
176: system is compared to that of \sys{dlv} which is a state-of-the-art
177: system for disjunctive programs.
178: \end{abstract}
179:
180: %------------------------------------------------------------------------------
181:
182: \section{INTRODUCTION}
183:
184: Implementation techniques for declarative semantics of logic programs
185: have advanced considerably during the last years. For example, the
186: XSB system~\cite{SSW96:jicslp} is a WAM-based full logic programming system
187: supporting the well-founded semantics. In addition to this kind of a
188: skeptical approach that is based on query evaluation also a credulous
189: approach focusing on computing models of logic programs is gaining
190: popularity. This work has been centered around the stable model
191: semantics~\cite{GL88:iclp,GL91:ngc}.
192: %
193: There are reasonably efficient implementations
194: available for computing stable models for disjunctive and normal
195: (disjunction-free) programs, e.g.,
196: %
197: \sys{dlv}~\cite{DLV},
198: \sys{smodels}~\cite{SMODELS,SNS02:aij},
199: \sys{cmodels}~\cite{CMODELS}, and
200: \sys{assat}~\cite{LZ02:aaai}.
201: %
202: The implementations have provided a basis for a new paradigm for logic
203: programming called \emph{answer set programming} (a term coined by
204: Vladimir Lifschitz).
205: %
206: The basic idea is that a problem
207: is solved by devising a logic program such that the stable models
208: of the program provide the answers to the problem, i.e.,
209: solving the problem is reduced to a stable model computation
210: task~\cite{Lifschitz99:iclp,MT99:lpp,Niemela99:amai,EGM97:acmtds,BLR97:lpnmr}.
211: This approach has led to interesting applications in areas such as
212: planning~\cite{DNK97:planning,EFLPP2000:cl,BBGBW01:padl}, model
213: checking~\cite{LRS98:tacas,Heljanko99:fi}, and software
214: configuration~\cite{Syrjanen00:cl}.
215:
216: This paper addresses two issues in the stable model semantics:
217: partiality and disjunctions. The idea is to develop methodology such
218: that efficient procedures for computing (total) stable models that are
219: emerging can be exploited when dealing with partial stable models and
220: disjunctive programs.
221: %
222: Sometimes it is
223: natural to use partial stable models to represent a domain. Even when
224: working with total stable models, partial stable models could be
225: useful, e.g., for debugging purposes to show what is wrong in a
226: program without any total stable models. However, little has been
227: done on implementing the computation of partial stable models and most
228: of the work has focused on query evaluation w.r.t.\ the well-founded
229: semantics. In the paper we show that total stable models can capture
230: partial stable models using a simple linear program transformation.
231: This transformation works also in the disjunctive case showing that
232: implementations of total stable models, e.g.\ \sys{dlv}, can be used for
233: computing partial stable models. Using a suitable transformation of
234: queries, a mechanism for query answering can be realized as well.
235:
236: Our translation is interesting in many respects. First, it should be
237: noted that the translation does not follow directly from the
238: complexity results already available. It has been shown, e.g., that
239: the problem of deciding whether a query is contained in some model
240: (possibility inference) is $\Sigma^p_2$-complete for both partial
241: and total stable models~\cite{EG95:amai,ELS98:tcs}. This
242: implies that there exists a polynomial time reduction from possibility
243: inference w.r.t.\ partial models to possibility inference w.r.t.\
244: total models. However, this kind of a translation is guaranteed to
245: preserve only the yes/no answer to the possibility inference problem.
246: %
247: Second, not all translations are satisfactory from a
248: computational point of view. In practice, when a program is compiled
249: into another form to be executed, certain computational properties of
250: the translation play an important role:
251: %
252: \begin{itemize}
253: \item
254: %
255: efficiency of the compilation (in which order of polynomial),
256: %
257: \item
258: %
259: modularity (are independent, separate compilations of parts of a
260: program possible), and
261: %
262: \item
263: %
264: structural preservation (are the composition and intuition of the
265: original program preserved so that debugging and understanding of
266: runtime behavior are made possible).
267: %
268: \end{itemize}
269: %
270: All this points to the importance of finding good translation methods
271: to enable the use of an existing inference engine to solve other
272: interesting problems.
273:
274: The efficiency of procedures for computing stable models of normal
275: programs has increased substantially in recent years. An interesting
276: possibility to exploit the computational power of such a procedure is
277: to use it as a {\em core engine} for implementing other reasoning
278: systems.
279: %
280: In this paper, we follow this approach and develop a method for
281: reducing stable model computation of disjunctive programs to the
282: problem of determining stable models for normal programs.
283: %
284: This is non-trivial as deciding whether a disjunctive program has a
285: stable model is $\Sigma^p_2$-complete~\cite{EG95:amai} whereas the
286: problem is $\NP$-complete in the non-disjunctive
287: case~\cite{MT91:jacm}.
288: %
289: The method has been implemented using the \sys{smodels} system
290: \cite{SMODELS,SNS02:aij} as the core engine. The performance of the
291: implementation is compared to that of \sys{dlv}, which is a
292: state-of-the-art system for computing stable models for disjunctive
293: programs.
294:
295: There are a number of novelties in the work. Maximal partial stable
296: models for normal programs are known as {\em regular models}, {\em
297: M-stable models}, and {\em preferred
298: extensions}~\cite{Dung95:jlp,Sacca90:pods,YY94:jcss}. Although this semantics
299: has a sound and complete top-down query answering
300: procedure~\cite{Dung95:jlp,EK89:iclp,LY01:ijcai}, so far very little effort
301: has been given to a serious implementation. For disjunctive programs,
302: to our knowledge, no implementation has ever been attempted. As a
303: result, we obtain (perhaps) the first scalable implementation of the
304: regular model/preferred extension semantics, and the first
305: implementation ever for partial stable model semantics for disjunctive
306: programs.
307: %
308: Our technical work on the relationship between stable and partial
309: stable models via a translational approach provides a compelling
310: argument for the naturalness of partial stable models: stable models
311: and partial stable models share the same notion of unfoundedness,
312: carefully studied earlier in~\cite{ELS97:amai,LRS97:ic}.
313: %
314: Finally, we demonstrate how key tasks in computing
315: disjunctive stable models can be reduced to stable model computation for
316: normal programs by suitable program transformations.
317: In particular, we develop techniques for mapping a disjunctive program
318: into a normal one such that the set of stable models of the normal
319: program covers the set of stable models of the disjunctive one and
320: in many case even coincides with it.
321: %
322: Moreover, we devise a method where the stability of a
323: model candidate for a disjunctive program can be determined by
324: transforming the disjunctive program into a normal one and checking the
325: existence of a stable model for it.
326: %
327: Finally, in the experimental part of this paper, we present a new way
328: of encoding quantified Boolean formulas as disjunctive logic programs.
329: This transformation is more economical in the number of propositional
330: atoms and disjunctive rules than earlier transformations presented in
331: the literature
332: %
333: \cite{EG95:amai,LPFEGPS03:submitted}.
334:
335: The rest of the paper is structured as follows.
336: %
337: We first review the basic definitions and concepts
338: in Section~\ref{section:definitions}.
339: %
340: It is then shown in Section~\ref{section:partiality} that partial
341: stable models can be captured with total stable models using a simple
342: program transformation.
343: %
344: In Section~\ref{section:disjunctions}, we describe the method for
345: computing disjunctive stable models using an implementation of
346: non-disjunctive programs as a core engine.
347: %
348: After this, we present some experimental results in
349: Section~\ref{section:experiments} and finish with concluding
350: remarks in Section~\ref{section:conclusions}.
351:
352: As a comment on the historical development of the translation given in
353: Section 3, the characterization of partial stable models as stable
354: models of the transformed program was first sketched for normal
355: programs in a proof by Schlipf \cite[Theorem 3.2]{Schlipf95:jcss}.
356: For disjunctive programs, it was discovered and proven in
357: \cite{SMR97:ilps}, and independently in \cite{JNSY00:kr}. In the
358: current paper we present a proof based on unfounded sets, which was
359: given in \cite{JNSY00:kr}, as this proof reveals some of the
360: properties of unfounded sets which are of interest in their own right.
361: %
362: Yet another approach to computing the partial stable models of a
363: disjunctive program based on a program transformation has been
364: developed by Ruiz and Minker \cite{RM95:nmelp}: a disjunctive program
365: $P$ is translated into a positive disjunctive program $P^{3S}$ with
366: constraints, the {\em 3S--transformation} of $P$, such that the total
367: minimal models of $P^{3S}$ that additionally fulfill the constraints
368: coincide with the partial stable models of $P$.
369:
370: %==============================================================================
371:
372: \section{DEFINITIONS AND NOTATIONS}
373: \label{section:definitions}
374:
375: A {\em disjunctive logic program} $P$ (or, just {\em disjunctive
376: program} $P$) is a set of rules of the form
377: %
378: \begin{equation}
379: \rg{a_1}{\lor}{a_k}\IF\rg{b_1}{,}{b_m},\rg{\naf c_1}{,}{\naf c_n}
380: \label{eq:drule}
381: \end{equation}
382: %
383: where $k \geq 1$, $m,n \geq 0$ and $a_i$'s, $b_i$'s and $c_i$'s are
384: atoms from the Herbrand base $\hb{P}$\footnote{For the sake of
385: convenience, we assume that a given program $P$ is already
386: instantiated by the underlying Herbrand universe, and is thus ground.}
387: of $P$.
388: %
389: Let us also distinguish subclasses of disjunctive programs. If $k=1$
390: for each rule of $P$, then $P$ is a {\em disjunction-free} or {\em
391: normal program}. If $n=0$ for each rule of $P$, then $P$ is called
392: {\em positive}.
393:
394: {\em Literals} are either atoms from $\hb{P}$ or expressions of the
395: form $\naf a$ where $a\in\hb{P}$. For a set of atoms
396: $A\subseteq\hb{P}$, we define $\naf A$ as $\sel{\naf a}{a\in A}$. Let
397: us introduce a shorthand $A\IF B,\naf C$ for rules where
398: $A\neq\emptyset$, $B$ and $C$ are subsets of $\hb{P}$. In harmony
399: with (\ref{eq:drule}), the set of atoms $A$ in the {\em head} of the
400: rule is interpreted disjunctively while the set of literals
401: $B\union\naf C$ in the {\em body} of the rule is interpreted
402: conjunctively.
403: %
404: We wish to further simplify the notation $A\IF B,\naf C$ in some
405: particular cases. When $A$, $B$ or $C$ is a singleton $\set{a}$, we
406: write $a$ instead of $\set{a}$. If $B=\emptyset$ or $C=\emptyset$ we
407: omit $B$ and $\naf C$ (respectively) as well as the separating comma
408: in the body of the rule.
409:
410: %------------------------------------------------------------------------------
411:
412: \subsection{PARTIAL AND TOTAL MODELS}
413:
414: We review the basic model-theoretic concepts by following the
415: presentation in \cite{ELS98:tcs}.
416: %
417: Let $P$ be any disjunctive program. A {\em partial interpretation} $I$
418: for $P$ is a pair $\pair{T}{F}$ of subsets of $\hb{P}$ such that
419: $T\isect F=\emptyset$. The atoms in the sets $\True{I}=T$,
420: $\False{I}=F$ and $\Undef{I}=\hb{P}-(T\union F)$ are considered to be
421: {\em true}, {\em false}, and {\em undefined}, respectively. We
422: introduce constants $\true$, $\false$, and $\undef$, to denote the
423: respective three truth values.
424: %
425: A partial interpretation $I$ for $P$ is a {\em total} interpretation
426: for $P$ whenever $\Undef{I}=\emptyset$, i.e., if every atom of
427: $\hb{P}$ is either true or false. When no confusion arises, we use
428: $\True{I}$ alone to specify a total interpretation $I$ for $P$ (then
429: $\False{I}=\hb{P}-\True{I}$ and $\Undef{I}=\emptyset$ hold).
430:
431: Given a partial interpretation for $P$, the truth values of atoms are
432: determined by $\True{I}$, $\False{I}$ and $\Undef{I}$ as explained
433: above while $\true$, $\false$ and $\undef$ have their fixed truth
434: values. For more complex logical expressions $E$, we use $\val{I}{E}$
435: to denote the truth value of $E$ in $I$. The value $\val{I}{\naf a}$
436: is defined to be $\true$, $\false$, or $\undef$ whenever $\val{I}{a}$
437: is $\false$, $\true$, or $\undef$, respectively.
438: %
439: To handle conjunctions and disjunctions, we introduce an ordering on
440: the three truth values by setting $\false<\undef<\true$. By default, a
441: set of literals $L=\eset{l_1}{l_n}$ denotes the conjunction
442: $\rg{l_1}{\land}{l_n}$ while $\Lor{L}$ denotes the corresponding
443: disjunction $\rg{l_1}{\lor}{l_n}$. The truth values $\val{I}{L}$ and
444: $\val{I}{\Lor{L}}$ are defined as the respective minimum and maximum
445: among the truth values $\rg{\val{I}{l_1}}{,}{\val{I}{l_n}}$.
446: %
447: A rule $A\IF B,\naf C$ is satisfied in $I$ if and only if
448: $\val{I}{\Lor{A}}\geq\val{I}{B\union\naf C}$.
449: %
450: A partial interpretation $M$ for $P$ is a {\em partial model} of $P$
451: if all rules of $P$ are satisfied in $M$, and for a {\em total model},
452: also $\Undef{M}=\emptyset$ holds. Let us then introduce an ordering
453: among partial models of a disjunctive program: $M_1\leq M_2$ if and only if
454: $\True{M_1}\subseteq\True{M_2}$ and $\False{M_1}\supseteq\False{M_2}$.
455: A partial model $M$ of $P$ is a {\em minimal} one if there is no
456: partial model $M'$ of $P$ such that $M'<M$ (i.e., $M'\leq M$ and
457: $M'\neq M$). In case of total models, we have $N_1\leq N_2$ if and only if
458: $N_1\subseteq N_2$. Moreover, a total model $N$ of $P$ is considered
459: to be a {\em minimal} one if there is no total model $N'$ of $P$ such
460: that $N'\subset N$.
461:
462: %------------------------------------------------------------------------------
463:
464: \subsection{STABLE MODELS}
465:
466: Given a partial interpretation $I$ for a disjunctive program $P$, we
467: define a reduction of $P$ as follows:
468: %
469: \[\GLred{P}{I}=
470: \sel{A\IF B}
471: {A\IF B,\naf C\in P\mbox{ and }
472: C\subseteq\False{I}} .
473: \]
474: %
475: Note that this transformation coincides with the {\em
476: Gelfond-Lifschitz reduction} of $P$ (the GL-reduction of $P$) when $I$
477: is a total interpretation.
478:
479: \begin{definition}[Total stable model]
480: \label{def:stablemodels}
481: %
482: A total interpretation $N$ for a disjunctive program $P$ is a stable
483: model if and only if $N$ is a minimal total model of $\GLred{P}{N}$.
484: \end{definition}
485:
486: The original definition of partial stable models \cite{Przymusinski90:iclp,Przymusinski90:fi}
487: is based on a weaker reduction. Given a disjunctive program $P$ and an
488: interpretation $I$, the reduction $\red{P}{I}$ is the set of rules
489: obtained from $P$ by replacing any $\naf c$ in the body of a rule by
490: $I(\naf c)$.
491: %
492: As noted in \cite{Przymusinski90:iclp}, the only practical difference between
493: $\GLred{P}{I}$ and $\red{P}{I}$ is that $\red{P}{I}$ has rules that
494: correspond to rules of $A\IF B,\naf C\in P$ satisfying
495: $\val{I}{\naf C}=\undef$. Note that if $\val{I}{\naf C}=\true$, then
496: $A\IF B\in\GLred{P}{I}$, and if $\val{I}{\naf C}=\false$, then
497: the partial models of $\red{P}{I}$ are not constrained by the rule
498: included in $\red{P}{I}$.
499:
500: \begin{definition}[Partial stable model]
501: \label{def:partial-stable}
502: A partial interpretation $M$ for a disjunctive program $P$ is a
503: partial stable model of $P$ if and only if $M$ is a minimal partial model of
504: $\red{P}{M}$.
505: \end{definition}
506:
507: In the above definition, the relation between $M$ and $\red{P}{M}$ is
508: similar to the one for the total stable model, both for the purpose of
509: preserving the stability condition. While maximizing falsity and
510: minimizing true atoms, a partial stable model does not insist that
511: every atom must be either true or false.
512: %
513: (Partial) stable models are intimately related to {\em unfounded
514: sets}~\cite{ELS97:amai,LRS97:ic}.
515:
516: \begin{definition}[Unfounded sets]
517: \label{def:unfounded-sets}
518: Let $I$ be a partial interpretation for a disjunctive program $P$.
519: %
520: A set $U\subseteq\hb{P}$ of ground atoms is an {\em unfounded set} for
521: $P$ w.r.t.\ $I$, if at least one of the following conditions holds for
522: each rule $A\IF B,\naf C\in P$ such that $A\isect U\neq\emptyset$:
523: %
524: \begin{description}
525: %
526: \item[\textnormal{\UFi:}]
527: %
528: $B\isect\False{I}\neq\emptyset$ or $C\isect\True{I}\neq\emptyset$,
529: %
530: \item[\textnormal{\UFii:}]
531: %
532: $B\isect U\not=\emptyset$, or
533: %
534: \item[\textnormal{\UFiii:}]
535: %
536: $(A - U)\isect(\True{I}\union\Undef{I})\neq\emptyset$.
537: %
538: \end{description}
539: %
540: An unfounded set $U$ for $P$ w.r.t.\ $I$ is $I$-consistent if
541: and only if $U\isect\True{I}=\emptyset$.
542: \end{definition}
543: %
544: The conditions \UFi\ and \UFiii\ above coincide with the conditions
545: %
546: \begin{center}
547: $\val{I}{B\union\naf C}=\false$ and $\val{I}{\Lor(A-U)}\neq\false$,
548: \end{center}
549: respectively.
550: %
551: The intuition is that the atoms of an unfounded set $U$ can be assumed
552: to be false without violating the satisfiability of any rule $A\IF
553: B,\naf C$ of the program whose head contains some atoms of $U$. For
554: any such rule, either
555: %
556: the rule body is false in $I$ (\UFi),
557: %
558: or the rule body can be falsified by falsifying the atoms in $U$ (\UFii),
559: %
560: or the head of the rule is not false in $I$ (\UFiii).
561: %
562: In particular, unfounded sets w.r.t.\ partial/total models can be used
563: for constructing smaller partial/total models (recall the definition
564: of minimal partial and total models) in a way that is made precise
565: by what follows.
566:
567: \begin{lemma}
568: \label{lemma:set-unfounded-false}
569: Let $M=\pair{T}{F}$ be a partial model of a positive disjunctive
570: program $P$ and $U$ an unfounded set for $P$ w.r.t.\ $M$.
571: %
572: Then, if $M$ is total or $U$ is $M$-consistent,
573: $M'=\pair{T-U}{F\union U}$ is a partial model of $P$.
574: \end{lemma}
575:
576: \begin{proof}
577: Let $M$, $P$, $U$ and $M'$ be defined as above. Additionally,
578: we assume that
579: %
580: (a)
581: %
582: $M$ is total, or
583: %
584: (b)
585: %
586: $U$ is $M$-consistent.
587: %
588: Let us then assume that some rule $A\IF B$ of $P$ is not
589: satisfied in $M'$ which means that
590: %
591: $\val{M'}{\Lor A}<\val{M'}{B}$.
592: %
593: Thus
594: %
595: (i)
596: %
597: $\val{M'}{\Lor A}<\true$ and $\val{M'}{B}=\true$, or
598: %
599: (ii)
600: %
601: $\val{M'}{\Lor A}=\false$ and $\val{M'}{B}=\undef$.
602: %
603: Our proof splits in two separate threads.
604:
605: \begin{itemize}
606:
607: \item[{\bf I.}]
608: %
609: Assume that $A\isect U=\emptyset$ holds.
610: %
611: Consider the case (i).
612: %
613: Now $\val{M'}{\Lor A}<\true$ implies $A\isect(T-U)=\emptyset$. Since
614: $A\isect U=\emptyset$ holds, too, we obtain $A\isect T=\emptyset$ so
615: that $\val{M}{\Lor A}<\true$. On the other hand, $\val{M'}{B}=\true$
616: implies $B\subseteq T-U$. Thus $B\subseteq T$ and $\val{M}{B}=\true$
617: holds as well. But then $\val{M}{\Lor A}<\val{M}{B}$, a contradiction.
618: %
619: The case (ii) is analyzed next.
620: %
621: Now $\val{M'}{\Lor A}=\false$ implies $A\subseteq F\union U$ as well
622: as $A\subseteq F$, since $A\isect U=\emptyset$. Thus $\val{M}{\Lor
623: A}=\false$. Moreover, from $\val{M'}{B}=\undef$ we obtain
624: $B\isect(F\union U)=\emptyset$. Thus we obtain $B\isect
625: F\neq\emptyset$ so that $\val{M}{B}>\false$ holds.
626: To conclude, we have established that
627: $\val{M}{\Lor A}<\val{M}{B}$, a contradiction.
628:
629: \item[{\bf II.}]
630: %
631: Otherwise $A\isect U\neq\emptyset$ holds. Then at least one of the
632: unfoundedness conditions is applicable to $A\IF B$. If \UFi\ is,
633: $\val{M}{B}=\false$ holds. It follows that $B\subseteq F$ and
634: $B\subseteq F\union U$. Thus $\val{M'}{B}=\false$ contradicting both
635: (i) and (ii).
636: %
637: If \UFii\ is applicable, we have $B\isect U\neq\emptyset$. It follows
638: that $B\isect(F\union U)\neq\emptyset$ so that $\val{M'}{B}=\false$, a
639: contradiction.
640:
641: Thus \UFiii\ must apply, i.e., $\val{M}{\Lor(A-U)}>\false$ holds.
642: Let us then consider cases (a) and (b) separately.
643: %
644: \begin{enumerate}
645: \item[(a)]
646: %
647: If $M$ is total, we have necessarily $\val{M}{\Lor(A-U)}=\true$. This
648: implies that some atom $a\in A-U$ belongs to $T$. Thus also $a\in T-U$
649: and $\val{M'}{\Lor A}=\true$, a contradiction with both (i) and (ii).
650:
651: \item[(b)]
652: %
653: If $U$ is $M$-consistent, we have $U\isect T=\emptyset$. By
654: $\val{M}{\Lor(A-U)}=\true$ there is an atom $a\in A-U$ such that
655: $a\not\in F$. Then $a\not\in F\union U$ which implies $\val{M'}{\Lor
656: A}>\false$. Thus (ii) is impossible and (i) implies $\val{M'}{\Lor
657: A}=\undef$ and $\val{M'}{B}=\true$. It follows that
658: $A\isect(T-U)=\emptyset$ and $B\subseteq T-U$. Since $U\isect
659: T=\emptyset$, the former implies $A\isect T=\emptyset$ while the
660: latter implies that $B\subseteq T$. Consequently, $\val{M}{\Lor
661: A}<\true$ and $\val{M}{B}=\true$, i.e., $\val{M}{\Lor A}<\val{M}{B}$,
662: a contradiction.
663: \end{enumerate}
664: \end{itemize}
665: \end{proof}
666:
667: Let us yet emphasize the content of Lemma
668: \ref{lemma:set-unfounded-false} when $M$ is total (and $U$ need not be
669: $M$-consistent). Then $M'=M-U$ is also a total model of $P$.
670: %
671: A couple of examples on unfounded sets follow.
672:
673: \begin{example}
674: Consider a disjunctive program
675: %
676: \[
677: P =\{ a \lor b \IF c, \naf a\}
678: \]
679: %
680: and an interpretation $I =\langle \emptyset, \{a\}\rangle$. The only
681: rule in $P$ has its body undefined in $I$, hence \UFi\ is not
682: applicable. The set $\{a\}$ is unfounded w.r.t.\ $I$ since $b$ is
683: undefined in $I$ and not in the set, hence \UFiii\ is applicable.
684: %
685: On the other hand, the set $\{b\}$ is not unfounded w.r.t.\ $I$ whereas
686: $\{c\}$ is unfounded w.r.t.\ $I$.
687: %
688: Once $c$ belongs to an unfounded set, the atoms $a$ and $b$ can both
689: get in due to \UFii. Hence, we have $U =\{a,b,c\}$ as an unfounded set
690: w.r.t.\ $I$.
691:
692: Comparing $U$ with $\False{I}$, we find that $\False{I}$ does not
693: maximize the atoms that should be false. This program $P$ has exactly
694: one stable model (which is also a partial stable model) in which all
695: three atoms are false.
696: %
697: \ebox
698: \end{example}
699:
700: Unlike the case for normal programs, the union of unfounded sets may
701: not be an unfounded set.
702: %
703: \begin{example}
704: Consider a program $P$ containing only one rule
705: %
706: \[
707: a \lor b \IF
708: \]
709: %
710: and an interpretation $I =\langle \{a,b\},\emptyset\rangle$. The
711: program has two non-empty unfounded sets w.r.t.\ $I$, $\{a\}$ and
712: $\{b\}$. Either $a$ or $b$ depends on the other one not in the set
713: for \UFiii\ to be applicable. However, \UFiii\ becomes not applicable when
714: both $a$ and $b$ are in, thus the union $\{a,b\}$ is not an unfounded
715: set.
716: %
717: \ebox
718: \end{example}
719:
720: An interpretation $I$ for $P$ becomes particularly interesting when
721: the union of all unfounded sets $U$ for $P$ w.r.t.\ $I$ is also an
722: unfounded set for $P$ w.r.t.\ $I$. In this case, the program $P$
723: possesses {\em the greatest unfounded} set $U$ for $P$ w.r.t.\ $I$.
724:
725: \begin{definition}
726: \label{def:unfounded-free}
727: A total interpretation $I$ is said to be {\em unfounded free} for a
728: program $P$ if and only if there is no unfounded set $U$ for $P$
729: w.r.t.\ $I$ such that $U\isect\True{I}\neq\emptyset$.
730: \end{definition}
731:
732: The notion of unfounded freeness captures the stable model
733: beautifully.
734: \begin{theorem} {\bf \cite{LRS97:ic}}
735: \label{theorem:SM-character}
736: %
737: Let $M$ be a total interpretation for a disjunctive program $P$.
738: Then, the following are equivalent
739: %
740: \begin{itemize}
741: \item
742: %
743: $M$ is a stable model of $P$.
744: %
745: \item
746: %
747: $\False{M}$ is the greatest unfounded
748: set for $P$ w.r.t.\ $M$.
749: %
750: \item
751: %
752: $M$ is unfounded free for $P$.
753: %
754: \end{itemize}
755: \end{theorem}
756:
757: On the other hand, Eiter et al. \cite{ELS97:amai} show that partial
758: stable models can be defined essentially without reference to
759: three-valued logic.
760:
761: \begin{theorem} {\bf \cite{ELS97:amai}}
762: \label{theorem:PSM-character}
763: %
764: If $M$ is a partial interpretation for a disjunctive program $P$,
765: then $M$ is a partial stable model of $P$ if and only if
766:
767: \begin{itemize}
768: %
769: \item
770: %
771: $\True{M}$ is a minimal total model of $\GLred{P}{M}$ and
772: %
773: \item
774: %
775: $\False{M}$ is a maximal $M$-consistent unfounded set for $P$ w.r.t.\ $M$.
776: \end{itemize}
777: \end{theorem}
778:
779: The first condition in the theorem is called {\em foundedness}
780: in \cite{ELS97:amai}.
781: %
782: The differences between these two theorems are quite subtle. The
783: strictness of stable models enforces a simpler relationship between
784: stable models and unfounded sets. Therefore, neither maximality nor
785: consistency nor foundedness need be explicitly stated. The characterization
786: of partial stable models in Theorem~\ref{theorem:PSM-character}
787: accounts for a more reflexible situation: since $M$ may not be a total
788: model, maximality should extend the set of false atoms as much as
789: possible without causing inconsistency. However, maximality and
790: consistency are still not strong enough.
791: %
792: \begin{example}
793: Consider a disjunctive program
794: %
795: \[
796: P = \{ a \lor b \IF \naf a\}
797: \]
798: %
799: and an interpretation $I = \langle \{a\}, \{b\} \rangle$ which is
800: total so that the definition of unfoundedness makes no difference in
801: valuation under $I$. Since the body of the rule is false in $I$, $U_1
802: = \{a\}$, $U_2 = \{b\}$, and $U_3 = \{a,b\}$ are all nonempty
803: unfounded sets in this case. It follows immediately by Theorem
804: \ref{theorem:PSM-character} that $I$ is not a stable model. However,
805: $U_2$ is maximally $I$-consistent yet it is not a partial stable model
806: because $\True{I}$ is not a minimal model of $P^I$.
807:
808: Note that $P$ has a unique (partial) stable model, which is $\langle
809: \{b\},\{a\}\rangle$.
810: %
811: \ebox
812: \end{example}
813:
814: The characterizations for partial and total stable models in terms of
815: unfounded sets provide a powerful tool for establishing relationships
816: between stable models and partial stable models.
817:
818: %==============================================================================
819:
820: \section{UNFOLDING PARTIALITY}
821: \label{section:partiality}
822:
823: In this section, we first show a translation for a disjunctive program
824: into another disjunctive program. We then prove that the translation
825: preserves the semantics of partial stable models. This result allows
826: us to compute the partial stable models of a program by computing the
827: stable models of the translated program. Finally we address the
828: problem of query answering under the translation.
829:
830: \subsection{TRANSLATION}
831:
832: Let $P$ be a disjunctive program. In the following, we describe a
833: translation of $P$ into another disjunctive program $\tr{}{P}$ such
834: that the stable models of $\tr{}{P}$ correspond to the partial stable
835: models of $P$.
836:
837: Let us introduce a new atom $\pot{a}$ for each $a\in\hb{P}$. An atom
838: $\pot{a}$ is said to be {\em marked}, and an ordinary atom $a$ is then
839: said to be {\em unmarked}. The intuitive reading of $\pot{a}$ is that
840: $a$ is {\em potentially} true.
841: %
842: For a set of literals $L \subseteq\hb{P} \cup \naf\hb{P}$, we define
843: %
844: $\pot{L}=\sel{\pot{a}}{a\in L} \union \sel{\naf \pot{a}}{\naf a\in L}$.
845: %
846: The translation $\tr{}{P}$ of a disjunctive program $P$ is as
847: follows:
848: %
849: \begin{multline}
850: \tr{}{P}=
851: \sel{A\IF B,\naf\pot{C}\END\pot{A}\IF\pot{B},\naf C}{A\IF B,\naf C\in P}
852: \ \union \\
853: \sel{\pot{a}\IF a}{a\in\hb{P}}
854: \end{multline}
855: %
856: where semicolons are used to separate program rules.
857: %
858: Note that the Herbrand base of $\hb{\tr{}{P}}$ is
859: $\hb{P}\union\pot{\hb{P}}$. The rules $\pot{a}\IF a$ introduced
860: for each $a\in\hb{P}$ enforce consistency in the sense that if $a$ is
861: true, then $a$ must also be potentially true.
862:
863: \begin{remark}
864: Although for presentational purposes the translation is defined for
865: ground programs, exactly the same translation applies to non-ground
866: programs as well: for each predicate $p$ we introduce a new predicate
867: $\pot{p}$, hence for a (ground or non-ground) atom $\phi =
868: p(\rg{t_1}{,}{t_n})$, the new atom is $\pot{\phi} =
869: \pot{p}(\rg{t_1}{,}{t_n})$ (cf. Example~\ref{barber}). Since our
870: proofs do not depend on the assumption that a given program is finite,
871: the conclusions reached cover also any non-ground program with
872: function symbols whose semantics is determined by treating the program
873: as a shorthand for its (possibly infinite) Herbrand instantation.
874: \end{remark}
875:
876: A partial stable model of a given program will be
877: interpreted by a corresponding stable model of the transformed
878: program.
879: %
880: The extra symbol $\pot{a}$ for each atom $a$ provides an opportunity
881: to represent {undefined} (in three-valued logic) in terms of truth
882: values of $\pot{a}$ and $a$ in two-valued logic. For each pair $a$ and
883: $\pot{a}$, either of which can be true or false, there are four
884: possibilities: when $\pot{a}$ and $a$ are in agreement, that is when
885: they are both true or both false, the truth value of $a$ is their
886: commonly agreed truth value; the combination where $a$ is false and
887: $\pot{a}$ is true then represents that $a$ is undefined; and the
888: fourth possibility where $a$ is true and $\pot{a}$ is false is ruled out by any
889: models due to the consistency rules.
890: %
891: This intended representation of a partial stable model is given by the
892: following equations.
893:
894: \begin{definition}
895: \label{def:CE1234}
896: Let $M$ be a partial interpretation of a program $P$
897: and $N$ a total interpretation of $\tr{}{P}$.
898: %
899: The interpretations $M$ and $N$ are said to satisfy the {\em
900: correspondence equations} if and only if the following equations hold.
901: \begin{align*}
902: \True{M} & =
903: \sel{a\in\hb{P}}{a\in\True{N}\mbox{ and }\pot{a}\in\True{N}}
904: \tag{CE1} \\
905: \False{M} & =
906: \sel{a\in\hb{P}}{a\in\False{N}\mbox{ and }\pot{a}\in\False{N}}
907: \tag{CE2} \\
908: \Undef{M} & =
909: \sel{a\in\hb{P}}{a\in\False{N}\mbox{ and }\pot{a}\in\True{N}}
910: \tag{CE3} \\
911: \emptyset & =
912: \sel{a\in\hb{P}}{a\in\True{N}\mbox{ and }\pot{a}\in\False{N}}
913: \tag{CE4}
914: \end{align*}
915: \end{definition}
916:
917: Note that total interpretations that are models of $\tr{}{P}$ satisfy
918: CE4 immediately, since the set of rules $\sel{\pot{a}\IF
919: a}{a\in\hb{P}}$ is included in $\tr{}{P}$. Consequently, the ``fourth
920: truth value'' is ruled out.
921: %
922: The following example demonstrates how the representation given in
923: Definition \ref{def:CE1234} allows us to capture the partial stable
924: models of a disjunctive program $P$ with the total stable models of
925: $\tr{}{P}$.
926:
927: \begin{example}
928: \label{ex:stable-models}
929: %
930: Consider a disjunctive program
931: %
932: \begin{center}
933: $P=\{a\lor b \IF \naf c\END
934: b \IF \naf b\END
935: c \IF \naf c\}$.
936: \end{center}
937: %
938: Now $a$ becomes false by the minimization of partial models, since the
939: falsity of $a$ does not affect the satisfiability of any rule. Thus
940: the unique partial stable model of $P$ is
941: $M=\pair{\emptyset}{\set{a}}$. Note that the reduction
942: %
943: $\red{P}{M}=
944: \set{a\lor b\IF\undef\END
945: b\IF\undef\END
946: c\IF\undef}$.
947: %
948: Then consider the translation
949: %
950: \[
951: \begin{array}{r@{\,}l@{\,}lll@{}l}
952: \tr{}{P}= & \{ & a \lor b\IF\naf\pot{c}\END
953: & b\IF\naf\pot{b}\END
954: & c\IF\naf\pot{c}\END \\
955: & & \pot{a}\lor\pot{b}\IF\naf c\END
956: & \pot{b}\IF\naf b\END
957: & \pot{c}\IF\naf c\END \\
958: & & \pot{a}\IF a\END
959: & \pot{b}\IF b\END
960: & \pot{c}\IF c & \}.
961: \end{array}
962: \]
963: %
964: The unique stable model of $\tr{}{P}$ is $N=\set{\pot{b},\pot{c}}$
965: which represents (by CE2 and CE3) the setting that $b$ and $c$ are
966: undefined and $a$ is false in $M$.
967: %
968: \ebox
969: \end{example}
970:
971: It is well-known that a disjunctive program $P$ may not have any
972: partial stable models. In such cases, the translation $\tr{}{P}$
973: should not have stable models either, if the translation $\tr{}{P}$ is
974: to be faithful.
975: %
976: \begin{example}
977: \label{ex:no-stable-models}
978: %
979: Consider a disjunctive program
980: %
981: \begin{center}
982: $P=\{a\lor b\lor c\IF\END
983: a\IF\naf b\END
984: b\IF\naf c\END
985: c\IF\naf a\}$
986: \end{center}
987: %
988: and its translation
989: %
990: \[
991: \begin{array}[t]{l@{\,}c@{\,}l@{\,}llll@{\,}ll}
992: \tr{}{P} & = &
993: \{ & a\lor b\lor c\IF\END & a\IF\naf \pot{b}\END
994: & b\IF\naf \pot{c}\END & c\IF\naf \pot{a}\END \\
995: && & \pot{a}\lor\pot{b}\lor\pot{c}\IF\END & \pot{a}\IF\naf b\END
996: & \pot{b}\IF\naf c\END & \pot{c}\IF\naf a
997: & \}\union C
998: \end{array}
999: \]
1000: %
1001: where
1002: $C=\{\pot{a}\IF a\END
1003: \pot{b}\IF b\END
1004: \pot{c}\IF c\}$
1005: %
1006: is the set of consistency rules.
1007:
1008: Consider a partial model $M=\pair{\set{a,b}}{\emptyset}$ of $P$ and a
1009: total model $N=\set{a,\pot{a},b,\pot{b},\pot{c}}$ of $\tr{}{P}$ that
1010: satisfy the equations CE1--CE4 in Definition \ref{def:CE1234}.
1011: %
1012: Now the reduced program $\red{P}{M}$ is
1013: %
1014: \[
1015: \{ a \lor b \lor c\IF\END
1016: a \IF \false\END
1017: b \IF \undef\END
1018: c \IF \false \}
1019: \] and since
1020: %
1021: $M'=\pair{\set{a,b}}{\set{c}}<M$ is a partial model of
1022: $\red{P}{M}$, $M$ is not a partial stable model of $P$.
1023: %
1024: On the other hand, the reduct
1025: %
1026: \[
1027: \GLred{\tr{}{P}}{N}=
1028: \{ a\lor b\lor c\IF\END
1029: \pot{a}\lor\pot{b}\lor\pot{c}\IF\END
1030: \pot{b}\IF \}\union C .
1031: \]
1032: %
1033: But $N'=\set{a,\pot{a},b,\pot{b}}\subset N$ is a model of
1034: $\GLred{\tr{}{P}}{N}$ so $N$ is not a stable model of $\tr{}{P}$.
1035: %
1036: The reader may analyze the other candidates in a similar fashion. It
1037: turns out that $P$ does not have partial stable models. Nor does
1038: $\tr{}{P}$ have stable models.
1039: %
1040: \ebox
1041: \end{example}
1042:
1043: Partial stable models can be viewed as a logic programming account of
1044: the solution of semantic paradoxes due to Kripke \cite{Kripke75:jp}. In
1045: this account, undefined means {\em unknown} for some individuals which
1046: will not lose semantic interpretations for other individuals.
1047: %
1048: \begin{example}
1049: \label{barber}
1050: Consider the following program with variables:
1051: %
1052: \[
1053: \begin{array}{l@{\ }c@{\ }lll}
1054: P & = & \{ &
1055: \at{shave}(\at{bob}, x)
1056: \IF \naf \at{shave}(x,x)\END\\
1057: &&& \at{pay\_by\_cash}(y,x) \lor \at{pay\_by\_credit}(y,x)
1058: \IF \at{shave}(x,y)\END\\
1059: &&& \at{accepted}(x,y)
1060: \IF \at{pay\_by\_cash}(x,y)\END\\
1061: &&& \at{accepted}(x,y)
1062: \IF \at{pay\_by\_credit}(x,y)\ \}. \\
1063: \end{array}
1064: \]
1065: %
1066: This program intuitively says that Bob shaves those who do not shave
1067: themselves; if $x$ shaves $y$ then $y$ pays $x$ by cash or by credit;
1068: either way is accepted. The predicate $\at{accepted}$ is used here to
1069: demonstrate disjunctive reasoning.
1070:
1071: Assume there is another person, called Greg. Then clearly, we
1072: should conclude Bob shaves Greg, and Greg pays Bob by cash or
1073: by credit, either way is accepted. However, the program has no stable
1074: models in this case due to the paradox whether Bob shaves
1075: himself or not. But it has two partial stable models, in both of which
1076: $\at{shave}(\at{greg},\at{greg})$ is false and
1077: $\at{shave}(\at{bob},\at{bob})$ is undefined (unknown).
1078: %
1079: By translating the first two rules of $P$ we obtain
1080: %
1081: \[
1082: \begin{array}{ll}
1083: \at{shaves}(\at{bob}, x)
1084: \IF \naf \pot{\at{shaves}} (x,x)\END \\
1085: \pot{\at{shaves}}(\at{bob}, x)
1086: \IF \naf \at{shaves}(x,x)\END \\
1087: \at{pay\_by\_cash}(y,x) \;\lor\; \at{pay\_by\_credit}(y,x)
1088: \IF \at{shaves}(x,y)\END \mbox{and} \\
1089: \pot{\at{pay\_by\_cash}}(y,x) \lor \pot{\at{pay\_by\_credit}}(y,x)
1090: \IF \pot{\at{shaves}}(x,y). \\
1091: \end{array}
1092: \]
1093: %
1094: The full translation $\tr{}{P}$ yields a Herbrand instantiation over
1095: the universe $\set{\at{bob},\at{greg}}$ which has four total stable
1096: models. One of them is
1097: %
1098: %
1099: \[
1100: \begin{array}{r@{\ }c@{\ }l@{\ }l}
1101: N & = & \{ &
1102: \pot{\at{shaves}}(\at{bob},\at{bob}), \\
1103: &&& \at{shaves}(\at{bob},\at{greg}),\ \pot{\at{shaves}}(\at{bob},\at{greg}), \\
1104: &&& \at{pay\_by\_cash}(\at{greg},\at{bob}),
1105: \ \pot{\at{pay\_by\_cash}}(\at{greg},\at{bob}), \\
1106: &&& \pot{\at{pay\_by\_credit}}(\at{bob},\at{bob}),
1107: \ \pot{\at{accepted}}(\at{bob},\at{bob}), \\
1108: &&& \at{accepted}(\at{greg},\at{bob}),\ \pot{\at{accepted}}(\at{greg},\at{bob})
1109: \ \}.
1110: \end{array}
1111: \]
1112: %
1113: Hence the fact that $\at{shaves}(\at{bob},\at{bob})$ is undefined in the
1114: corresponding partial stable model $M$ (recall the equations in
1115: Definition \ref{def:CE1234}) is represented by
1116: $\pot{\at{shaves}}(\at{bob},\at{bob})$ being true and
1117: $\at{shaves}(\at{bob},\at{bob})$ being false in $N$.
1118: %
1119: \ebox
1120: \end{example}
1121:
1122: %------------------------------------------------------------------------------
1123:
1124: \subsection{CORRECTNESS OF THE TRANSLATION}
1125:
1126: The goal of this section is to establish a one-to-one correspondence
1127: between the partial stable models of a disjunctive program $P$ and the
1128: (total) stable models of the translation $\tr{}{P}$.
1129: %
1130: It is first shown that the correspondence equations CE1--CE4 given in
1131: Definition~\ref{def:CE1234} provide a syntactic way to transform a
1132: partial stable model $M$ of $P$ into a total stable model $N$ of
1133: $\tr{}{P}$ and back. More formally, we have the following theorem in
1134: mind.
1135:
1136: \begin{theorem}
1137: \label{theorem:PSM-iff-SM}
1138: Let $M$ be a partial interpretation of a disjunctive program $P$ and
1139: $N$ a total interpretation of the translation $\tr{}{P}$ such that
1140: CE1--CE4 are satisfied.
1141: %
1142: Then $M$ is a partial stable model of $P$ if and only if $N$ is a
1143: (total) stable model of $\tr{}{P}$.
1144: \end{theorem}
1145:
1146: Our strategy to prove Theorem \ref{theorem:PSM-iff-SM} is as follows:
1147: first, in two separate lemmas, we show the correspondence, in each
1148: direction, between unfounded sets for $P$ and $\tr{}{P}$ under $M$ and
1149: $N$, respectively. These two lemmas are interesting in their own
1150: right as they show very tight conditions under which the two
1151: previously studied notions of unfoundedness
1152: \cite{ELS97:amai,LRS97:ic} are related. These results will then
1153: be used in the proof of the theorem.
1154: %
1155: We first state two relatively simple facts. The first says that that
1156: the GL-transform has no effect on unfoundedness, and the second states
1157: that the translation preserves models via CE1--CE4 in
1158: Definition \ref{def:CE1234}.
1159:
1160: \begin{proposition}
1161: \label{no-effect}
1162: Let $P$ be a disjunctive program and $N$ a total
1163: interpretation for $P$.
1164: %
1165: Then, $X\subseteq\hb{P}$ is an unfounded set for $P$ w.r.t.\ $N$
1166: if and only if
1167: $X$ is an unfounded set for $\GLred{P}{N}$ w.r.t.\ $N$.
1168: \end{proposition}
1169:
1170: \begin{proof}
1171: Note that $A\IF B\in\GLred{P}{N}$ if and only if there is a rule $A\IF
1172: B,\naf C\in P$ such that $C\subseteq\False{N}$, i.e.,
1173: $C\isect\True{N}=\emptyset$.
1174: %
1175: Then it holds for any $X\subseteq\hb{P}$ that
1176: %
1177: \begin{center}
1178: \begin{tabular}{cl}
1179: & $X$ is not an unfounded set for $P$ w.r.t.\ $N$ \\
1180: $\iff$
1181: &
1182: $\exists A\IF B,\naf C\in P$ such that (1) $A\isect X\neq\emptyset$,
1183: (2) $B\isect\False{N}=\emptyset$, \\ & (3) $C\isect\True{N}=\emptyset$,
1184: (4) $B\isect X=\emptyset$, and (5) $(A-X)\isect\True{N}=\emptyset$ \\
1185: $\iff$
1186: &
1187: $\exists A\IF B\in\GLred{P}{N}$ such that (6) $A\isect X\neq\emptyset$,
1188: (7) $B\isect\False{N}=\emptyset$, \\ & (8) $B\isect
1189: X=\emptyset$, and (9) $(A-X)\isect\True{N}=\emptyset$ \\
1190: $\iff$
1191: &
1192: $X$ is not an unfounded set for $\GLred{P}{N}$ w.r.t.\ $N$.
1193: \end{tabular}
1194: \end{center}
1195: \end{proof}
1196:
1197: \begin{proposition}
1198: \label{model-for-M-N}
1199: Let $M$ be a partial interpretation for a disjunctive program $P$ and
1200: $N$ a total interpretation for the translation $\tr{}{P}$. Assume
1201: $M$ and $N$ satisfy the CEs. Then, $M$ is a partial model of $P$ if
1202: and only if $N$ is a total model of $\tr{}{P}$.
1203: \end{proposition}
1204:
1205: \begin{proof}
1206: It follows by the correspondence equations CE1--CE4 in Definition
1207: \ref{def:CE1234} that $M$ is not a partial model of $P$ if and only if
1208: %
1209: \begin{center}
1210: \begin{tabular}{@{}cl@{}}
1211: &
1212: $\exists$ $A\IF B,\naf C\in P$:\
1213: $\val{M}{\Lor{A}}<\val{M}{B\union\naf C}$ \\
1214: %
1215: $\iff$ &
1216: $\exists$ $A\IF B,\naf C\in P$:\
1217: $\val{M}{\Lor{A}}<\true$ and $\val{M}{B\union\naf C}=\true$, {\em or} \\
1218: &
1219: $\exists$ $A\IF B,\naf C\in P$:\
1220: $\val{M}{\Lor{A}}=\false$ and $\val{M}{B\union\naf C}=\undef$ \\
1221: %
1222: $\iff$ &
1223: $\exists$ $A\IF B,\naf\pot{C}\in\tr{}{P}$:\
1224: $\val{N}{\Lor{A}}=\false$ and $\val{N}{B\union\naf\pot{C}}=\true$, {\em or} \\
1225: &
1226: $\exists$ $\pot{A}\IF\pot{B},\naf C\in\tr{}{P}$:\
1227: $\val{N}{\Lor{\pot{A}}}=\false$ and $\val{N}{\pot{B}\union\naf C}=\true$ \\
1228: $\iff$ &
1229: $\exists$ $A\IF B,\naf\pot{C}\in\tr{}{P}$:\
1230: $\val{N}{\Lor{A}}<\val{N}{B\union\naf\pot{C}}$, {\em or} \\
1231: &
1232: $\exists$ $\pot{A}\IF\pot{B},\naf C\in\tr{}{P}$:\
1233: $\val{N}{\Lor{\pot{A}}}<\val{N}{\pot{B}\union\naf C}$
1234: \end{tabular}
1235: \end{center}
1236: which is equivalent to stating that $N$ is not a total
1237: model of $\tr{}{P}$, since the consistency rules in $\tr{}{P}$
1238: are automatically satisfied by CE4.
1239: \end{proof}
1240:
1241: Still assuming the setting determined by CEs, the following lemma
1242: gives a condition under which the unfounded sets w.r.t.\ $N$ for
1243: $\tr{}{P}$ can be converted into unfounded sets w.r.t.\ $M$ for $P$.
1244:
1245: \begin{lemma}
1246: \label{lemma:UF-to-PUF}
1247: %
1248: Let $P$ be a program, $M$ a partial interpretation of $P$ and
1249: $N$ a total interpretation of the program $\tr{}{P}$ such that
1250: CE1--CE4 are satisfied.
1251: %
1252: Then, for any unfounded set $X$ for $\tr{}{P}$ w.r.t.\ $N$,
1253: the set of atoms $Y=\sel{a\in\hb{P}}{\pot{a}\in X}$
1254: %
1255: is an unfounded set for $P$ w.r.t.\ $M$.
1256: %
1257: In addition, if $X$ is $N$-consistent,
1258: then $Y$ is $M$-consistent.
1259: \end{lemma}
1260:
1261: \begin{proof}
1262: Consider any rule $A\IF B,\naf C\in P$ such that $A\isect
1263: Y\neq\emptyset$. It is proven in the sequel that one of the
1264: unfoundedness conditions \UFi--\UFiii\ applies to $A\IF B,\naf C$.
1265: %
1266: Two cases arise depending on the value of $\val{M}{B\union\naf C}$.
1267:
1268: \begin{itemize}
1269: %
1270: \item[\bf I.]
1271: %
1272: If $\val{M}{B\union\naf C}=\false$, then
1273: \UFi\ is directly applicable.
1274:
1275: \item[\bf II.]
1276: %
1277: Suppose that $\val{M}{B\union\naf C}\neq\false$ which
1278: implies $\val{N}{\pot{B}\union\naf C}=\true$ by the CEs.
1279: %
1280: Now $A\isect Y\neq\emptyset$ and the definition of $Y$ imply
1281: $\pot{A}\isect X\neq\emptyset$.
1282: %
1283: Since $\pot{A}\IF\pot{B},\naf C\in\tr{}{P}$, $X$ is an unfounded set
1284: for $\tr{}{P}$ w.r.t.\ $N$ and \UFi\ is not applicable to
1285: $\pot{A}\IF\pot{B},\naf C$, we know that either \UFii\ or \UFiii\
1286: applies to $\pot{A}\IF\pot{B},\naf C$.
1287: %
1288: \begin{enumerate}
1289: %
1290: \item[(i)]
1291: %
1292: If \UFii\ applies to $\pot{A}\IF\pot{B},\naf C$, then $\pot{B}\isect
1293: X\neq\emptyset$. It follows by the definition of $Y$ that $B\isect
1294: Y\neq\emptyset$, i.e., \UFii\ applies to $A\IF B,\naf C$.
1295:
1296: \item[(ii)]
1297: %
1298: If \UFiii\ applies to $\pot{A}\IF\pot{B},\naf C$, then
1299: $\val{N}{\Lor(\pot{A}-X)}=\true$. Since $\pot{A}-X=\pot{(A-Y)}$ by the
1300: definition of $Y$, we obtain by the CEs that $\val{M}{\Lor(A-Y)}\neq\false$.
1301: Thus \UFiii\ applies to $A\IF B,\naf C$.
1302:
1303: \end{enumerate}
1304: \end{itemize}
1305:
1306: The proof of the consistency claim follows.
1307: %
1308: To establish the contrapositive of the claim, suppose that $Y$ is not
1309: $M$-consistent. Then $Y\isect\True{M}\neq\emptyset$, i.e., there
1310: exists an atom $a\in\hb{P}$ such that $a\in Y$ and $a\in\True{M}$.
1311: %
1312: The former implies $\pot{a}\in X$ by the definition of $Y$ while the
1313: latter gives us $\pot{a}\in\True{N}$ by the CEs.
1314: %
1315: Thus $X\isect\True{N}\neq\emptyset$ and $X$
1316: is not $N$-consistent.
1317: \end{proof}
1318:
1319: The next lemma shows that, under the specified conditions, an
1320: unfounded set for a given disjunctive program $P$ corresponds to a
1321: collection of unfounded sets for the translation $\tr{}{P}$.
1322:
1323: \begin{lemma}
1324: \label{lemma:PUF-to-UF}
1325: Let $M$ be a partial model of a disjunctive program $P$ and
1326: $N$ a total interpretation of $\tr{}{P}$ satisfying the CEs.
1327: %
1328: If $X$ is an $M$-consistent unfounded set for $P$ w.r.t.\ $M$,
1329: then $Y=F \union U$ where $F=\sel{a,\pot{a}}{a \in X}$ and
1330: $U\subseteq\sel{a}{a\in\False{N},\pot{a}\in\True{N}}$
1331: is an unfounded set for $\tr{}{P}$ w.r.t.\ $N$.
1332: \end{lemma}
1333:
1334: \begin{proof}
1335: Let $X$ be an $M$-consistent unfounded set for $P$ w.r.t.\ $M$ and let
1336: $Y=F\union U$ satisfy the requirements above. Since any atom in $Y$ is
1337: either marked or unmarked, two cases arise.
1338:
1339: \begin{itemize}
1340: %
1341: \item[\bf I.]
1342: %
1343: Suppose that $\pot{a}\in Y$ which implies
1344: by the definition of $Y$ that $a\in Y$.
1345: %
1346: Then it is clear that that \UFii\ applies to the consistency rule
1347: $\pot{a}\IF a\in\tr{}{P}$.
1348: %
1349: Let us then prove that one of the unfoundedness conditions applies to
1350: any rule $\pot{A}\IF\pot{B},\naf C\in \tr{}{P}$ satisfying
1351: $\pot{a}\in\pot{A}$.
1352: %
1353: Since $N$ is a total interpretation, we have
1354: $\val{N}{\pot{B}\union\naf C}=\false$ (in which case \UFi\ applies to
1355: $\pot{A}\IF\pot{B},\naf C$) or $\val{N}{\pot{B}\union\naf C}=\true$ in
1356: which case $\val{M}{B\union\naf C}>\false$. Since $a\in X$ and $a\in
1357: A$, and \UFi\ does not apply to $A\IF B,\naf C$, we only need to
1358: consider \UFii\ and \UFiii.
1359: %
1360: If \UFii\ applies to $A\IF B,\naf C$, $\exists b \in B$ such that $b
1361: \in X$. It follows by the definition of $Y$ that $\pot{b}\in Y$.
1362: Hence \UFii\ applies to $\pot{A}\IF\pot{B},\naf C$.
1363: %
1364: If \UFiii\ applies to $A\IF B,\naf C$, $\exists b \in A$ such that
1365: $\val{M}{b}>\false$ and $b\not\in X$. Then we know that
1366: $\val{N}{\pot{b}}=\true$ by the CEs. Further, by the definition of
1367: $Y$, $b \not \in X$ implies $\pot{b} \not \in Y$. Hence \UFiii\
1368: applies to $\pot{A}\IF\pot{B},\naf C$.
1369:
1370: \item[\bf II.]
1371: %
1372: Suppose that $a \in Y$.
1373: %
1374: Then consider any rule $A\IF B,\naf\pot{C}\in \tr{}{P}$ such that
1375: $a\in A$. Since $N$ is a total interpretation,
1376: $\val{N}{B\union\naf\pot{C}}=\false$ (in which case \UFi\ applies to
1377: $A\IF B,\naf\pot{C}$) or $\val{N}{B\union\naf\pot{C}}=\true$.
1378: %
1379: In the latter case, we know that $\exists b\in A$ such that
1380: $\val{N}{b}=\true$, since $N$ is a model of $\tr{}{P}$ by
1381: Proposition~\ref{model-for-M-N}
1382: (recall that $M$ is a partial model of $P$).
1383: %
1384: Then suppose that $b\in Y$, i.e., $b \in F$ or $b \in U$ by the
1385: definition of $Y$.
1386: %
1387: If $b\in F$, then $b \in X$ by the definition of $F$. On the
1388: other hand, $\val{N}{b}=\true$ implies $\val{M}{b}=\true$.
1389: Thus $\True{M}\isect X\neq\emptyset$, contradicting the
1390: $M$-consistency of $X$.
1391: %
1392: If $b\in U$, the the definition of $U$ implies $\val{N}{b}=\false$, a
1393: contradiction.
1394: %
1395: Hence, $b\not\in Y$ and \UFiii\ applies to $A\IF B,\naf\pot{C}$.
1396: \end{itemize}
1397: \end{proof}
1398:
1399: We note that the $M$-consistency of $X$ is also a necessary condition
1400: for the correspondence to hold.
1401:
1402: \begin{example}
1403: Consider a disjunctive program
1404: %
1405: $
1406: P = \set{ a \lor b \IF;\ a \IF \naf a }
1407: $
1408: %
1409: and a partial model $M =\pair{\set{b}}{\emptyset}$ of $P$.
1410: %
1411: It can be checked easily that $X=\set{b}$ is an unfounded set for $P$
1412: w.r.t.\ $M$: \UFiii\ applies to the only rule in which $b$ appears in
1413: the head. But $X$ is not $M$-consistent. Now consider
1414: %
1415: \[
1416: \begin{array}{r@{\,}c@{\,}lll@{}l}
1417: \tr{}{P} & =\{ & a \lor b \IF;
1418: & \pot{a} \lor \pot{b} \IF;
1419: & a \IF \naf \pot{a}; \\
1420: & & \pot{a} \IF \naf a;
1421: & \pot{a} \IF a;
1422: & \pot{b} \IF b & \}. \\
1423: \end{array}
1424: \]
1425: %
1426: The total interpretation corresponding to $M$ above is
1427: $N=\set{\pot{a},b,\pot{b}}$. However, $Y=\set{a,b,\pot{b}}$ is not
1428: unfounded for $\tr{}{P}$ w.r.t.\ $N$, since for $b \in Y$ and the
1429: first rule in $\tr{}{P}$, none of the unfoundedness conditions
1430: applies.
1431: %
1432: \ebox
1433: \end{example}
1434:
1435: Let us establish Theorem \ref{theorem:PSM-iff-SM} in two separate theorems.
1436:
1437: \begin{theorem}
1438: \label{theorem:SM-to-PSM}
1439: Let $P$ be a disjunctive program.
1440: %
1441: If $N$ is a stable model of the translation $\tr{}{P}$, then the
1442: partial interpretation $M$ of $P$ satisfying the correspondence
1443: equations CE1--CE4 is a partial stable model of $P$.
1444: \end{theorem}
1445:
1446: \begin{proof}
1447: Let $N$ be a stable model of $\tr{}{P}$.
1448: %
1449: Then it follows by the presence of consistency rules
1450: %
1451: $\sel{\pot{a}\IF a}{a\in\hb{P}}$
1452: %
1453: in $\tr{}{P}$ that there is no $a\in\hb{P}$ such that $a\in N$ and
1454: $\pot{a}\not\in N$, since $N$ is a total model of $\tr{}{P}$.
1455: %
1456: Thus it makes sense to define $M$ as the partial interpretation
1457: satisfying CE1--CE4. We prove that $\True{M}$ is a minimal total
1458: model of $\GLred{P}{M}$, and $\False{M}$ is a maximal $M$-consistent
1459: unfounded set for $P$ w.r.t. $M$.
1460:
1461: \begin{itemize}
1462: %
1463: \item[\bf I.]
1464: %
1465: Let us first establish that for any rule $A\IF B,\naf C\in P$, $A\IF
1466: B\in\GLred{P}{M}$ $\iff$ $A\IF B\in\GLred{\tr{}{P}}{N}$. So consider
1467: any $A\IF B,\naf C\in P$.
1468: %
1469: It follows by the CEs and the definitions of $\GLred{P}{M}$,
1470: $\tr{}{P}$ and $\GLred{\tr{}{P}}{N}$ that
1471: %
1472: $A\IF B\in\GLred{P}{M}$
1473: %
1474: $\iff$
1475: %
1476: there is a rule $A\IF B,\naf D\in P$ such that $D\subseteq\False{M}$
1477: %
1478: $\iff$
1479: %
1480: there is a rule $A\IF B,\naf\pot{D}\in\tr{}{P}$ such that
1481: $\pot{D}\subseteq\False{N}$
1482: %
1483: $\iff$
1484: %
1485: $A\IF B\in\GLred{\tr{}{P}}{N}$.
1486: %
1487: Note that within these equivalences $A\IF B,\naf C$ and $A\IF B,\naf
1488: D$ need not be the same rules of $P$.
1489:
1490: \item[\bf II.]
1491: %
1492: Let us then prove that $\True{M}$ is a minimal total model of
1493: $\GLred{P}{M}$. If we assume the contrary, two cases arise.
1494:
1495: \begin{itemize}
1496: %
1497: \item
1498: %
1499: $\True{M}$ is not a total model of $\GLred{P}{M}$, i.e., there is a
1500: rule $A\IF B\in\GLred{P}{M}$ such that $\val{\True{M}}{B}=\true$, but
1501: $\val{\True{M}}{A}=\false$. It follows by the CEs that
1502: $\val{N}{B}=\true$ and $\val{N}{A}=\false$. Thus $A\IF B$ is not
1503: satisfied in $N$ and thus $N$ is not a model of $\GLred{\tr{}{P}}{N}$,
1504: as $\GLred{P}{M}\subset\GLred{\tr{}{P}}{N}$ holds by (\textbf{I})
1505: above. A contradiction, since $N$ is a stable model of $\tr{}{P}$.
1506:
1507: \item
1508: %
1509: There is a total model $M'$ of $\GLred{P}{M}$ such that
1510: $M'\subset\True{M}$. Then define a total interpretation
1511: %
1512: $N'= M'\union\sel{\pot{a}}{\pot{a} \in N}$.
1513: %
1514: By $M' \subset \True{M}$ and the CEs, we obtain $N'\subset N$
1515: (only some unmarked atoms of $N$ are not in $N'$).
1516: %
1517: Since $M'$ is a total model of $\GLred{P}{M}$, and $M'$ and $N'$
1518: coincide on the atoms of $\hb{P}$, every rule in $\GLred{P}{M}$ is
1519: satisfied by $N'$.
1520: %
1521: By (\textbf{I}), the difference $\GLred{\tr{}{P}}{N}-\GLred{P}{M}$
1522: contains only consistency rules $\pot{a}\IF a$ (for every
1523: $a\in\hb{P}$) and rules of the form $\pot{A}\IF\pot{B}$ (for some
1524: $A\IF B,\naf C\in P$). These rules are all satisfied by $N'$, since
1525: $N$ is a total model of $\GLred{\tr{}{P}}{N}$, $N'\subset N$, and $N'$
1526: and $N$ coincide on the marked atoms in $\pot{\hb{P}}$. Thus $N'$ is
1527: a total model of $\GLred{\tr{}{P}}{N}$. Then $N'\subset N$ implies
1528: that $N$ is not a minimal model of $\GLred{\tr{}{P}}{N}$ nor a total
1529: stable model of $P$. A contradiction.
1530: \end{itemize}
1531:
1532: \item[\bf III.]
1533: %
1534: Since $N$ is a total stable model of $\tr{}{P}$, it holds by Theorem
1535: \ref{theorem:SM-character} that $\False{N}$ is the greatest unfounded
1536: set for $\tr{}{P}$ w.r.t.\ $N$. Moreover, $\False{N}$ is
1537: $N$-consistent, since $\False{N}\isect\True{N}=\emptyset$.
1538: %
1539: Note that $\pot{a}\in\False{N}$ implies $a\in\False{N}$,
1540: since $N$ satisfies $\pot{a}\IF a\in\tr{}{P}$. Thus
1541: %
1542: $\False{M}=
1543: \sel{a\in\hb{P}}{a\in\False{N}\mbox{ and }\pot{a}\in\False{N}}=
1544: \sel{a\in\hb{P}}{\pot{a}\in\False{N}}$.
1545: %
1546: It follows by Lemma~\ref{lemma:UF-to-PUF} that $\False{M}$ is an
1547: $M$-consistent unfounded set for $P$ w.r.t.\ $M$.
1548:
1549: Then assume that $\False{M}$ is not maximal, i.e., there is an
1550: $M$-consistent unfounded set $X$ for $P$ w.r.t.\ $M$ such that $X
1551: \supset\False{M}$. So there is an atom $a\in X$ such that $a\not \in
1552: \False{M}$. Then $a\not\in\False{M}$ implies $a\in\True{M}$ or $a
1553: \in\Undef{M}$. In both cases, by the CEs, $\pot{a}\in\True{N}$,
1554: i.e., $\pot{a}\not\in\False{N}$.
1555: %
1556: Then construct $Y=\sel{a,\pot{a}}{a\in X}$. According to
1557: Lemma~\ref{lemma:PUF-to-UF}, that $X$ is an $M$-consistent
1558: unfounded set for $P$ w.r.t.\ $M$ implies that $Y$ is an unfounded set
1559: for $\tr{}{P}$ w.r.t $N$. However, $a\in X$ implies $\pot{a}\in Y$
1560: but $\pot{a}\not\in \False{N}$. Thus $\pot{a}\in\True{N}$ indicating
1561: that $N$ is not unfounded free for $\tr{}{P}$. Consequently, $N$ is
1562: not a stable model of $\tr{}{P}$ by the characterization of stable
1563: models in Theorem \ref{theorem:SM-character}, a contradiction.
1564:
1565: \end{itemize}
1566: \end{proof}
1567:
1568: \begin{theorem}
1569: \label{theorem:PSM-to-SM}
1570: Let $P$ be a disjunctive program.
1571: %
1572: If $M$ is a partial stable model of $P$, then the total interpretation
1573: $N$ satisfying the correspondence equations CE1--CE4 is a stable model
1574: of the translation $\tr{}{P}$.
1575: \end{theorem}
1576:
1577: \begin{proof}
1578: Suppose that $M$ is a partial stable model of $P$. Then we know by
1579: Theorem \ref{theorem:PSM-character} that (i) $\True{M}$ is a minimal
1580: total model of $\GLred{P}{M}$ and (ii) $\False{M}$ is a maximal
1581: $M$-consistent unfounded set for $P$ w.r.t.\ $M$.
1582: %
1583: Then define $N$ as the total interpretation of $\tr{}{P}$ satisfying
1584: the CEs. It follows by Lemma \ref{lemma:PUF-to-UF} that
1585: $\False{N}=\sel{a,\pot{a}}{a\in\False{M}}\union\Undef{M}$ is an
1586: unfounded set for $\tr{}{P}$ w.r.t.\ $N$.
1587:
1588: Let us then assume that $N$ is not a stable model of $\tr{}{P}$.
1589: %
1590: Equivalently, it holds by Theorem \ref{theorem:SM-character} that
1591: $\False{N}$ is not the greatest unfounded set for $\tr{}{P}$
1592: w.r.t. $N$. So there is an unfounded set $X$ for $\tr{}{P}$ w.r.t.\
1593: $N$ such that $\False{N}\subset X$ and $\True{N}\isect X\neq\emptyset$
1594: hold. It follows by Proposition~\ref{no-effect} that $X$ is also an
1595: unfounded set for $\GLred{\tr{}{P}}{N}$ w.r.t. $N$.
1596:
1597: Then consider any $A\IF B\in\GLred{P}{M}$ for which there is a rule
1598: $A\IF B,\naf C\in P$ such that $C\subseteq\False{M}$. It follows by
1599: the CEs that $\pot{C}\subseteq\False{N}$. Since $A\IF
1600: B,\naf\pot{C}\in\tr{}{P}$, it follows that $A\IF
1601: B\in\GLred{\tr{}{P}}{N}$. Thus
1602: $\GLred{P}{M}\subset\GLred{\tr{}{P}}{N}$ holds, as
1603: $\GLred{\tr{}{P}}{N}$ contains among others the consistency rules
1604: $\sel{\pot{a}\IF a}{a\in\hb{P}}$.
1605:
1606: Recall that $\True{M}=\True{N}\isect\hb{P}$ is a minimal total model
1607: of $\GLred{P}{M}$. We also distinguish a set of atoms
1608: $X'=X\isect\hb{P}$. Let us then establish that $X'$ is an unfounded
1609: set for $\GLred{P}{M}$ with respect to $\True{M}$ in the two-valued sense.
1610: %
1611: \begin{itemize}
1612: %
1613: \item[{\bf I.}]
1614: %
1615: If $X'$ is not such a set, it follows by Definition
1616: \ref{def:unfounded-sets} that there is $A\IF B\in\GLred{P}{M}$ with
1617: $A\isect X'\neq\emptyset$ such that $B\subseteq\True{M}$, $B\isect
1618: X'=\emptyset$ and $(A-X')\isect\True{M}=\emptyset$.
1619: %
1620: It follows that $A\IF B\in\GLred{\tr{}{P}}{N}$, as
1621: $\GLred{P}{M}\subset\GLred{\tr{}{P}}{N}$. Since $A$ and $B$ are
1622: subsets of $\hb{P}$, $\True{M}=\True{N}\isect\hb{P}$ and
1623: $X'=X\isect\hb{P}$, we obtain $A\isect X\neq\emptyset$,
1624: $B\subseteq\True{N}$, $B\isect X=\emptyset$ and
1625: $(A-X)\isect\True{N}=\emptyset$. Then $X$ is not
1626: an unfounded set for $\GLred{\tr{}{P}}{N}$ w.r.t.\ $N$,
1627: a contradiction.
1628: %
1629: \end{itemize}
1630: %
1631: It follows by Lemma \ref{lemma:set-unfounded-false} that $\True{M}-X'$
1632: is a total model of $\GLred{P}{M}$. It follows by the minimality of
1633: $\True{M}$ that $\True{M}\isect X'=\emptyset$ and $\True{M}\isect
1634: X=\emptyset$.
1635: %
1636: Moreover, it follows by Lemma~\ref{lemma:UF-to-PUF} that
1637: $Y=\sel{a\in\hb{P}}{\pot{a}\in X}$ is an unfounded set for $P$ w.r.t.\
1638: $M$. It remains to establish that $Y$ is $M$-consistent and
1639: $\False{M}\subset Y$.
1640: %
1641: \begin{itemize}
1642: %
1643: \item[\bf II.]
1644: %
1645: Suppose that $Y$ is not $M$-consistent, i.e., it holds for some
1646: $\at{a}\in\hb{P}$ that (a) $a\in Y$ and (b) $a\in\True{M}$.
1647: %
1648: Now (b) implies by the CEs that $a\in\True{N}$ and
1649: $\pot{a}\in\True{N}$.
1650: %
1651: On the other hand, it follows by (a) and the definition of $Y$ that
1652: $\pot{a}\in X$. Thus one of the unfoundedness conditions applies to
1653: the rule $\pot{a}\IF a\in\tr{}{P}$, as $X$ is an unfounded set for
1654: $\tr{}{P}$ w.r.t.\ $N$.
1655: %
1656: Now \UFi\ is not applicable, as $\at{a}\not\in\False{N}$, and \UFiii\
1657: is not applicable, as $\pot{a}\in X$. Thus \UFii\ must be applicable
1658: to $\pot{a}\IF a$. It follows that $\at{a}\in X$, too. Then there is
1659: $a\in\hb{P}$ such that $a\in\True{M}$ and $a\in X$. A contradiction
1660: with $\True{M}\isect X=\emptyset$ established above.
1661:
1662: \item[\bf III.]
1663: %
1664: Consider any $a\in\False{M}$. Thus $a\in\hb{P}$ and
1665: $\pot{a}\in\False{N}$ follows by the CEs. Then $\False{N}\subset X$
1666: implies $\pot{a}\in X$ as well as $a\in Y$ by the definition of $Y$.
1667: Thus $\False{M}\subseteq Y$.
1668: %
1669: On the other hand, recall that $\True{N}\isect X\neq\emptyset$ and
1670: $\True{M}\isect X=\emptyset$. Then $\pot{a}\in \True{N}\isect X$ holds
1671: for some $a\in\hb{P}$. It follows that $\pot{a}\in\True{N}$ and
1672: $\pot{a}\in X$. The former implies $\at{a}\not\in\False{M}$ by the
1673: CEs. The latter implies $a\in Y$ by the definition of $Y$. Hence
1674: $\False{M}\subset Y$.
1675: %
1676: \end{itemize}
1677: %
1678: Thus $\False{M}$ is not a maximal $M$-consistent unfounded set for $P$
1679: w.r.t.\ $M$, a contradiction.
1680: %
1681: Hence $N$ must be a stable model of $\tr{}{P}$.
1682: \end{proof}
1683:
1684: It is worthwhile at this point to briefly comment on the proof of
1685: Theorem~\ref{theorem:PSM-iff-SM} as given in \cite{SMR97:ilps}, which
1686: proceeds in several steps. Given two partial interpretations
1687: $M$ and $M'$ of a disjunctive program $P$, let $N$ and $N'$,
1688: respectively, be the corresponding total interpretations of
1689: $\tr{}{P}$ such that CE1--CE4 are satisfied.
1690: %
1691: Firstly, it can be shown that $M$ is a partial model of $\red{P}{M'}$
1692: if and only if $N$ is a total model of $\GLred{\tr{}{P}}{N'}$.
1693: %
1694: Secondly, since the truth-ordering for partial
1695: interpretations corresponds to the subset ordering for total
1696: interpretations, it can be shown that
1697: the minimal partial models of $\red{P}{M'}$ correspond to
1698: the minimal total models of $\GLred{\tr{}{P}}{N'}$.
1699: %
1700: Thirdly, based on a characterization of partial models in general
1701: \cite{SMR97:ilps}, we conclude that $M$ is a partial stable model of
1702: $P$ if and only if $N$ is a total stable model of $\tr{}{P}$.
1703:
1704: Looking back to results established so far, we know by Theorem
1705: \ref{theorem:PSM-to-SM} that any partial stable model $M$ of $P$ can
1706: be mapped to a stable model
1707: %
1708: \begin{equation}
1709: \label{eq:expand}
1710: f(M)=\True{M}\union\pot{(\True{M}\union\Undef{M})}
1711: \end{equation}
1712: %
1713: of $\tr{}{P}$. Similarly, any stable model $N$ of $\tr{}{P}$
1714: can be projected to a partial stable model
1715: %
1716: \begin{equation}
1717: \label{eq:project}
1718: g(N)=
1719: \pair{\sel{a\in\hb{P}}{a\in N}}
1720: {\sel{a\in\hb{P}}{a\not\in N\mbox{ and }\pot{a}\not\in N}}
1721: \end{equation}
1722: %
1723: of $P$ by Theorem \ref{theorem:SM-to-PSM}. These equations and the
1724: corresponding theorems indicate that $f$ and $g$ are functions between
1725: the set of partial stable models of $P$ and the set of stable models
1726: of $\tr{}{P}$. In the sequel, it is established that these functions
1727: are bijections, which means that our translation technique does not
1728: yield spurious models for programs although new atoms are used. This
1729: is highly desirable from the knowledge representation perspective.
1730:
1731: \begin{theorem}
1732: \label{theorem:one-to-one-correspondece}
1733: The partial stable models of a disjunctive program $P$
1734: and the total stable models of the translation $\tr{}{P}$
1735: are in a one-to-one correspondence.
1736: \end{theorem}
1737:
1738: \begin{proof}
1739: Let $f$ and $g$ be defined by the equations (\ref{eq:expand}) and
1740: (\ref{eq:project}), respectively. It is straightforward to see that
1741: $f$ is injective, i.e., $f(M_1)=f(M_2)$ implies $M_1=M_2$.
1742: %
1743: Then assume that $g(N_1)=g(N_2)$ holds for some stable models $N_1$
1744: and $N_2$ of $\tr{}{P}$. It follows by the definition of $g$ for
1745: any $a\in\hb{P}$ that (i) $a\in N_1$ $\iff$ $a\in N_2$ and (ii)
1746: $a\not\in N_1$ and $\pot{a}\not\in N_1$ $\iff$ $a\not\in N_2$ and
1747: $\pot{a}\not\in N_2$.
1748: %
1749: Then consider any $a\in\hb{P}$ such that $\pot{a}\in N_1$. Two cases
1750: arise. If $a\in N_1$, it follows by (i) that $a\in N_2$. Since $N_2$
1751: satisfies the rule $\pot{a}\IF a\in\GLred{\tr{}{P}}{N_2}$, we obtain
1752: $\pot{a}\in N_2$. On the other hand, if $a\not\in N_1$ it follows by
1753: (i) that $a\not\in N_2$. Assuming that $\pot{a}\not\in N_2$ implies by
1754: (ii) that $\pot{a}\not\in N_1$, a contradiction. Hence $\pot{a}\in
1755: N_2$ also in this case. By symmetry, $\pot{a}\in N_2$ implies
1756: $\pot{a}\in N_1$.
1757:
1758: Thus it holds for any $a\in\hb{P}$ that (iii) $\pot{a}\in N_1$ $\iff$
1759: $\pot{a}\in N_2$. It follows by (i) and (iii) that $N_1=N_2$ so that
1760: $g$ is injective, too. Thus $f$ and $g$ are bijections and
1761: inverses of each other, as $g(f(M))=M$ and $f(g(N))=N$ hold
1762: for any (partial) stable models $M$ and $N$. Hence the claim.
1763: \end{proof}
1764:
1765: None of the preceding proofs relies on the assumption that the given
1766: program is finite. Therefore, all of these results presented in this
1767: section apply in the non-ground case as well.
1768:
1769: %------------------------------------------------------------------------------
1770:
1771: \subsection{QUERY ANSWERING}
1772:
1773: Let us yet address the possibility of using an inference engine for
1774: computing total stable models to answer queries concerning partial
1775: stable models. This is highly interesting, because there are already
1776: systems available for computing total stable models
1777: %
1778: \cite{CMODELS,LZ02:aaai,DLV,SNS02:aij}
1779: %
1780: while partial stable models lack
1781: implementations. Here we must remind the reader that partial stable
1782: models can be used in different ways in order to evaluate queries.
1783: Typically two modes of reasoning are used: {\em certainty inference}
1784: and {\em possibility inference}. In the former approach, a query $Q$
1785: should be true in all (intended) models of $P$ while $Q$ should be
1786: true in some (intended) model of $P$ in the latter approach. Moreover,
1787: maximal partial stable models (under set inclusion) are sometimes
1788: distinguished; this is how {\em regular models} and {\em preferred
1789: extensions} are obtained for normal
1790: %
1791: programs~\cite{Dung95:jlp,Sacca90:pods,YY94:jcss}.
1792: %
1793: We are particularly interested in possibility inference where the
1794: maximality condition makes no difference (see
1795: \cite{ELS98:tcs,Sacca97:jcss} for certainty inference):
1796: $\val{M}{Q}=\true$ for some partial stable model $M$ of $P$ if and only if
1797: $\val{M'}{Q}=\true$ for some maximal partial stable model $M'$ of $P$.
1798:
1799: We consider queries $Q$ that are sets of literals over $\hb{P}$ and
1800: queries are translated in harmony with the CEs:
1801: $\tr{}{Q}=Q\union\pot{Q}$. As a direct consequence of Theorem
1802: \ref{theorem:PSM-to-SM} and CE1, we obtain the following.
1803: %
1804: \begin{corollary}
1805: A query $Q$ is true in a (maximal) partial stable model
1806: of $P$ if and only if $\tr{}{Q}$ is true in a stable model of $\tr{}{P}$.
1807: \end{corollary}
1808:
1809: What about using a query answering procedure for partial stable models
1810: to answer queries concerning stable models? A slight extension of the
1811: translation $\tr{}{P}$ is needed for this purpose: let $\tr{2}{P}$ be
1812: $\tr{}{P}$ augmented with a set of rules $\sel{f\IF\pot{a},\naf
1813: a}{a\in\hb{P}}$ where $f\not\in\hb{P}$ is a new atom. The purpose of
1814: these additional rules is to detect partial stable models with
1815: remaining undefined atoms. A query $Q$ is translated into
1816: $\tr{2}{Q}=Q\union\set{\naf f}$.
1817: %
1818: \begin{corollary}
1819: A query $Q$ is true in a stable model of $P$ if and only if
1820: $\tr{2}{Q}$ is true in a partial stable model of $\tr{2}{P}$.
1821: \end{corollary}
1822:
1823: This result allows query answering for stable models to be conducted
1824: by a procedure for partial stable models, e.g., by the abductive
1825: procedure of Eshghi and Kowalski \cite{EK89:iclp}.
1826:
1827: %==============================================================================
1828:
1829: \section{UNFOLDING DISJUNCTIONS}
1830: \label{section:disjunctions}
1831:
1832: In this section we develop a method for reducing the task of computing
1833: a (total) stable model of a disjunctive program to computing stable
1834: models for normal (disjunction-free) programs. This objective demands
1835: us to {\em unfold}\,\footnote{The idea of unfolding disjunction
1836: generally refers to performing some transformations on disjunctions in
1837: order to remove them \cite{BD99:jlp,DGM96:fi,SS97:jlp}. However, such
1838: transformations do not necessarily remove all disjunctions or do not
1839: preserve stable semantics.} disjunctions from programs in a way or
1840: another.
1841: %
1842: Since the problem of deciding whether a disjunctive program has a
1843: stable model is $\Sigma^p_2$-complete~\cite{EG95:amai} whereas the
1844: problem is $\NP$-complete in the non-disjunctive
1845: case~\cite{MT91:jacm}, the reduction cannot be computable in
1846: polynomial time unless the polynomial hierarchy collapses. This is why
1847: our reduction is based on a generate and test approach.
1848:
1849: The basic idea is that given a disjunctive program $P$ we compute its
1850: stable models in two phases: (i) we \emph{generate} model candidates
1851: and (ii) \emph{test} candidates for stability until we find a suitable
1852: model. For generating model candidates we construct a normal program
1853: $\gen{P}$ such that the stable models of $\gen{P}$ give the candidate
1854: models. For testing a candidate model $M$ we build another normal
1855: program $\test{P}{M}$ such that $\test{P}{M}$ has no stable models
1856: if and only if
1857: $M$ is a stable model of the original disjunctive program $P$.
1858: %
1859: Hence, given a procedure for computing stable models for normal
1860: programs all stable models of a disjunctive program $P$ can be
1861: generated as follows: for each stable model $M$ of $\gen{P}$, decide
1862: whether $\test{P}{M}$ has a stable model and if this is not the case,
1863: output $M$ as a stable model of $P$.
1864: %
1865: This kind of a generate and test approach is used also in \sys{dlv}~\cite{DLV}
1866: which is a state-of-the-art system for disjunctive programs.
1867: The difference is that we reduce the test and generate subtasks directly
1868: to problems of computing stable models of normal programs whereas
1869: in \sys{dlv} special techniques for the two subtasks have been
1870: developed based on the notion of unfounded sets for disjunctive
1871: programs.
1872:
1873: It is easy to construct a normal program for generating
1874: candidate models for a disjunctive program $P$.
1875: Consider, e.g., a program $\genO{P}$ which contains
1876: for each atom $a \in \hb{P}$, two rules $a \IF \naf \hat{a}\END \hat{a}
1877: \IF \naf a$ where $\hat{a}$ is a new atom
1878: denoting the complement of the atom $a$, i.e., $a$ is in a stable model
1879: exactly when $\hat{a}$ is not.
1880: %
1881: These rules generate stable models
1882: corresponding to every subset of $\hb{P}$. In order to prune this set
1883: of models to those with all rules in $P$ satisfied, it is sufficient
1884: to include a rule
1885: %
1886: \begin{equation}
1887: f \IF \naf f, \naf a_1,\ldots,\naf a_k,b_1,\ldots,
1888: b_m, \naf c_1,\ldots, \naf c_n
1889: \label{eq:consistency}
1890: \end{equation}
1891: %
1892: for each rule of the form~(\ref{eq:drule}) in $P$ where $f$ is a new
1893: atom. As $f$ cannot be in any stable model, the rule functions as an
1894: integrity constraint eliminating the models where each $b_i$ is
1895: included, every $c_j$ is excluded but no $a_l$ is included.
1896:
1897: In order to guarantee completeness, it is sufficient that for each
1898: stable model $M$ of $P$ there is a corresponding model candidate which
1899: agrees with $M$ w.r.t.\ $\hb{P}$. It is clear that $\genO{P}$
1900: satisfies this condition. However, for efficiency
1901: it is important to devise a generating program that has as few as
1902: possible (candidate) stable models provided that completeness is not
1903: lost.
1904: %
1905: An obvious shortcoming of $\genO{P}$ is that it generates many
1906: candidates even if the program $P$ is disjunction-free.
1907: In order to solve this problem
1908: we construct
1909: for given a disjunctive program $P$ a generating program $\genI{P}$ as
1910: follows:
1911: %
1912: \begin{eqnarray*}
1913: \genI{P} & = &
1914: \begin{array}[t]{@{}l@{}}
1915: \{a \IF \naf \hat{a}, B, \naf C \mid A \IF B, \naf C \in \dlp{P}, a
1916: \in A \} \union \mbox{} \\
1917: \{\hat{a}\IF \naf a \mid a \in \heads{\dlp{P}} \} \union \mbox{} \\
1918: \{f \IF \naf f, \naf A, B, \naf C \mid
1919: A \IF B, \naf C \in \dlp{P} \} \cup
1920: \nlp{P}
1921: \end{array}
1922: \end{eqnarray*}
1923: %
1924: where $\nlp{P}$ is the set of the normal rules in $P$ and $\dlp{P}$ are
1925: the other
1926: (proper disjunctive) rules in $P$, i.e.\ $P = \nlp{P} \cup \dlp{P}$, and
1927: $\heads{\dlp{P}}$ is the set of atoms appearing in the heads of the rules in
1928: $\dlp{P}$.
1929:
1930: The program $\genI{P}$ has typically far fewer stable models than
1931: $\genO{P}$ and the number of ``extra'' candidate models which do not
1932: match stable models of $P$ is related to the number of
1933: disjunctions in $P$.
1934: %
1935: For example, if $P$ is disjunction-free,
1936: the stable models of $\genI{P}$ correspond exactly to the stable
1937: models of $P$.
1938: %
1939: However, for a disjunctive program $P$, $\genI{P}$ can easily have
1940: ``extra'' stable models.
1941: Consider, e.g.,
1942: %
1943: \begin{equation}
1944: P = \{ a \lor b \IF \}
1945: \label{eq:disjunction}
1946: \end{equation}
1947: %
1948: for which
1949: %
1950: $\genI{P} = \{
1951: a \IF \naf \hat{a}\END \hat{a} \IF \naf{a}\END
1952: b \IF \naf \hat{b}\END \hat{b} \IF \naf{b}\END
1953: f \IF \naf f, \naf a, \naf b\} $
1954: %
1955: has a stable model, $\{a,b\}$, not corresponding to a stable model of
1956: $P$.
1957: In fact, $\genI{P}$ only requires for each proper disjunctive rule in $P$
1958: that some non-empty subset of the head atoms of the rule is included in
1959: the model candidate when the body of the rule holds. Hence, for such a rule
1960: with $d$ disjuncts in the head there are $2^d -1$
1961: possible subsets and in the worst case $2^d - 2$ of these could lead to
1962: ``extra'' model candidates.
1963: This means that in the worst case $\genI{P}$ can have an exponential
1964: number of ``extra'' model candidates w.r.t.\ the number of disjunctions
1965: in $P$.
1966:
1967: In order to decrease the number of ``extra'' models we introduce
1968: a technique exploiting a key property of {\em supported models}
1969: \cite{BD97:jlp}: each atom $a$ true in a model $M$ of $P$ must have
1970: a rule {\em supporting} it, i.e., there is a rule $A\IF B,\naf C\in P$
1971: such that $a\in A$, $\val{M}{B\union\naf C}=\true$, and
1972: $\val{M}{\Lor(A-\set{a})}=\false$.
1973: Since every stable model of $P$ is also a supported model of $P$, it
1974: makes perfect sense to require supportedness from the candidate
1975: stable models.
1976: %
1977: For this, we introduce a new atom $\supp{a}$, which denotes the fact
1978: that atom $a$ has a supporting rule, for each atom $a$ appearing in the
1979: head of a disjunctive rule. The
1980: intuition behind the set of rules $\support{P}$ below is that a rule can
1981: support exactly one of its head atoms and we may exclude every model
1982: that has an atom without a supporting rule:
1983: %
1984: \begin{multline}
1985: \support{P} = \\
1986: \{\supp{a} \IF \naf (A-\{a\}), B, \naf C \mid A \IF B, \naf C \in P, a
1987: \in A \isect \heads{\dlp{P}}\}
1988: \ \union \\
1989: \{f \IF \naf f, a, \naf \supp{a} \mid a \in \heads{\dlp{P}} \}
1990: \end{multline}
1991: %
1992: where $\heads{\dlp{P}}$ is the set of atoms appearing in the heads of
1993: the proper disjunctive rules in $P$.
1994: %
1995: For example, for $P$ in (\ref{eq:disjunction}),
1996: \begin{center}
1997: $\support{P} = \{\supp{a} \IF \naf b\END \supp{b} \IF \naf a\END
1998: f \IF \naf f, a, \naf \supp{a}\END
1999: f \IF \naf f, b, \naf \supp{b} \}$.
2000: \end{center}
2001: %
2002: Now $\genI{P} \cup \support{P}$ has
2003: exactly two stable models $\{a,\supp{a}, \hat{b}\}$ and $\{b, \supp{b}, \hat{a}\}$
2004: corresponding to the two stable models $\{a\}$ and
2005: $\{b\}$ of $P$.
2006:
2007: Combining this idea with $\genI{P}$ gives a promising generating program
2008: \begin{equation}
2009: \gen{P} = \genI{P} \cup \support{P}
2010: \label{eq:gen}
2011: \end{equation}
2012: which still preserves completeness.
2013:
2014: \begin{proposition}
2015: Let $P$ be a disjunctive program. Then if $M$ is a stable model
2016: of $P$, there is a stable model $N$ of $\gen{P} = \genI{P} \cup \support{P}$
2017: with $M=N\isect\hb{P}$.
2018: \end{proposition}
2019:
2020: \begin{proof}
2021: Let $M$ be a stable model of $P$ and
2022: %
2023: \[N=M \union \sel{\hat{a}}{a\in\heads{\dlp{P}}-M} \union
2024: \sel{\supp{a}}{a\in M\isect \heads{\dlp{P}}}.\]
2025: %
2026: Now clearly $M=N\isect\hb{P}$.
2027: We show first that (i) $N$ is a model
2028: of $\GLred{\gen{P}}{N}$ and then that
2029: (ii) if there is a model $N'$ of $\GLred{\gen{P}}{N}$ such that $N' \subseteq N$
2030: then $N \subseteq N'$ holds.
2031: These together imply that $N$ is a stable model of $\gen{P}$.
2032:
2033: For property~(i) consider rules in
2034: $\GLred{\gen{P}}{N} = \GLred{\genI{P}}{N} \cup \GLred{\support{P}}{N}$
2035: starting with those in $\GLred{\genI{P}}{N}$.
2036: %
2037: Suppose $a \IF B \in \GLred{\genI{P}}{N}$. If $a \in \heads{\dlp{P}}$,
2038: then $\hat{a} \not\in N$ and, hence,
2039: $a \in M \subseteq N$. Otherwise if $a \not\in \heads{\dlp{P}}$, then
2040: $a \IF B \in \GLred{P}{M}$ implying that $N (\supseteq M)$ satisfies
2041: $a \IF B$.
2042: %
2043: If $\hat{a} \IF \in \GLred{\genI{P}}{N}$, then $a \not\in M$ and
2044: $\hat{a} \in N$.
2045: If $f \IF B \in \GLred{\genI{P}}{N}$, then there is a rule
2046: $ A \IF B, \naf C \in \dlp{P}$ such that
2047: $A \isect M = \emptyset$ and $A \IF B \in \GLred{P}{M}$.
2048: As $M$ is a model of $\GLred{P}{M}$, $B
2049: \not\subseteq M$ and, consequently, $B \not\subseteq N$.
2050: Thus, $N$ is a model of $\GLred{\genI{P}}{N}$.
2051: Next consider rules in $\GLred{\support{P}}{N}$.
2052: If $\supp{a} \IF B \in \GLred{\support{P}}{N}$, then there is a rule
2053: $ A \IF B, \naf C \in P$ such that
2054: $A \IF B \in \GLred{P}{M}$ and $(A - \{a\}) \isect M = \emptyset$.
2055: If $B \subseteq N$, then $B \subseteq M$ and, hence, $A \isect M \not=
2056: \emptyset$ as $M$ is a model of $\GLred{P}{M}$. Thus, $a \in M$.
2057: If $ f \IF a \in \GLred{\support{P}}{N}$, then $\supp{a} \not\in N$, and $a
2058: \not \in N$. This implies that $N$ is a model of $\GLred{\support{P}}{N}$
2059: and that (i) holds.
2060:
2061: For property~(ii) consider a model $N'$ of $\GLred{\gen{P}}{N}$ such
2062: that $N' \subseteq N$.
2063: %
2064: First we show that $N'\isect \hb{P}$ is a model of $\GLred{P}{M}$
2065: implying that $ M \subseteq N'\isect \hb{P}$.
2066: Consider $A \IF B \in \GLred{P}{M}$. If the body $B$ is true in
2067: $N'\isect \hb{P} \subseteq N \isect \hb{P} = M$,
2068: then at least one $a\in
2069: A\isect M$. Then $a\IF B \in \GLred{\gen{P}}{N}$ and $a\in
2070: N'$. Hence, $M \subseteq N'\isect \hb{P}$.
2071: If $\hat{a} \in N$, then $a \not\in N$ and, hence,
2072: $\hat{a} \IF \in \GLred{\genI{P}}{N}$ implying $\hat{a} \in N'$.
2073: %
2074: If $\supp{a} \in N$, then $a \in M\isect \heads{\dlp{P}}$. Then there is a rule
2075: $A \IF B \in \GLred{P}{M}$ such that $B \subseteq M$ but $(A -\{a\})
2076: \isect M = \emptyset$. This is because otherwise $M - \{a\}$ would be a
2077: model of $\GLred{P}{M}$ contradicting the minimality of $M$.
2078: Hence, $\supp{a} \IF B \in \GLred{\support{P}}{N}$ and $B \subseteq M
2079: \subseteq N'$ implying $\supp{a} \in N'$. Thus,
2080: $N \subseteq N'$ and (ii) holds.
2081: \end{proof}
2082:
2083: A (total) model candidate $M \subseteq \hb{P}$ is a stable model of a
2084: program $P$ if it is a minimal model of the GL-transform $\GLred{P}{M}$ of the
2085: program. This test can be reduced to an unsatisfiability problem in
2086: propositional logic using techniques presented
2087: in~\cite{Niemela96:tab}: $M$ is a minimal model of $P^M$ if and only if
2088: %
2089: \begin{equation}
2090: P^M \union \{\neg a \mid a \in \hb{P}-M\}
2091: \union
2092: \{\neg b_1 \lor \cdots\lor \neg b_m\}
2093: \label{eq:min-test}
2094: \end{equation}
2095: %
2096: is unsatisfiable where $M = \{ b_1 ,\ldots, b_m\}$ and the rules in
2097: $P^M$ are seen as clauses. This can be determined by testing
2098: non-existence of stable models for a normal program $\test{P}{M}$
2099: which is constructed for a disjunctive program $P$ and a total
2100: interpretation $M \subseteq \hb{P}$ as follows:
2101: \[
2102: \begin{array}{@{}l@{}}
2103: \test{P}{M} =
2104: \begin{array}[t]{l@{}}
2105: \{a \IF \naf\hat{a}, B \mid \begin{array}[t]{@{}l@{}}
2106: A \IF B \in \dlp{P}^M,
2107: a \in A \isect M, B \subseteq M \} \union \mbox{}
2108: \end{array}
2109: \\
2110: \{\hat{a}\IF \naf a \mid a \in \heads{\dlp{P}} \} \union \mbox{} \\
2111: \{f \IF \naf f, \naf A, B \mid \begin{array}[t]{@{}l@{}}
2112: A \IF B \in \dlp{P}^M,
2113: B \subseteq M \} \union \mbox{}
2114: \end{array}
2115: \\
2116: \{a \IF B \in \nlp{P}^M \mid \begin{array}[t]{@{}l@{}}
2117: a \in M, B \subseteq M \} \union \mbox{}
2118: \end{array}
2119: \\
2120: \{f \IF \naf f, M \}
2121: \end{array}
2122: \end{array}
2123: \]
2124: where $\nlp{P}$ is the set of the normal rules in $P$ and $\dlp{P}$ are
2125: the proper disjunctive rules in $P$ and
2126: $\heads{\dlp{P}}$ is the set of atoms appearing in the heads of the rules in
2127: $\dlp{P}$.
2128: %
2129: The idea is that stable models of $\test{P}{M}$ capture models of the reduct
2130: $P^M$ that are properly included in $M$.
2131:
2132: \begin{proposition}
2133: \label{prop:mintest}
2134: Let $P$ be a disjunctive program and $M$ a (total) model of $P$.
2135: Then $M$ is a minimal model of $P^M$
2136: if and only if
2137: $\test{P}{M}$ has no stable model.
2138: \end{proposition}
2139:
2140: \begin{proof}
2141: Let $M \subseteq \hb{P}$ be a total model of $P$.
2142:
2143: ($\Rightarrow$)
2144: %
2145: Let $N$ be a stable model of $\test{P}{M}$. If $a\in\hb{P}-M$, then
2146: there is no rule with $a$ in the head in $\test{P}{M}$ and $a \not\in N$.
2147: Hence, $N\isect\hb{P}\subseteq M$. As $f\not\in N$ and
2148: $f\IF M \in\GLred{\test{P}{M}}{N}$, there is some $a\in M$ such
2149: that $a\not\in N\isect\hb{P}$.
2150: %
2151: Consider $A \IF B \in \GLred{P}{M}$.
2152: %
2153: Let $B\subseteq N\isect\hb{P}\subseteq M$ but suppose $A\isect
2154: N\isect\hb{P} =\emptyset$.
2155: If $A = \{a\}$, $a \IF B\in\GLred{\test{P}{M}}{N}$ and $a \in N$, a
2156: contradiction. Otherwise $f\IF B\in\GLred{\test{P}{M}}{N}$ and
2157: $f\in N$, a contradiction. Hence, $N\isect\hb{P}$ is a model of
2158: $\GLred{P}{M}$ but $N\isect\hb{P}\subset M$ implying that $M$ is not a
2159: minimal model of $\GLred{P}{M}$.
2160:
2161: ($\Leftarrow$)
2162: %
2163: Assume that $M$ is not a minimal model of $\GLred{P}{M}$. As $M$ is a
2164: model of $\GLred{P}{M}$, there is a minimal model $M'\subset M$ of
2165: $\GLred{P}{M}$.
2166: %
2167: We show that
2168: %
2169: $N=M'\union\sel{\hat{a}}{a\in\heads{\dlp{P}}-M'}$
2170: %
2171: is a minimal model of $\GLred{\test{P}{M}}{N}$,
2172: i.e., $N$ a stable model of $\test{P}{M}$. Now
2173: $\GLred{\test{P}{M}}{N}=$
2174: %
2175: \[
2176: \begin{array}[t]{@{}l@{}}
2177: \{a \IF B \mid \begin{array}[t]{@{}l@{}}
2178: A \IF B \in \dlp{P}^M,
2179: a \in A \isect M \isect M', B \subseteq M \} \union \mbox{}
2180: \end{array}
2181: \\
2182: \{\hat{a}\IF \mid a \in \heads{\dlp{P}}-M' \}
2183: \union \mbox{} \\
2184: \{f \IF B \mid \begin{array}[t]{@{}l@{}}
2185: A \IF B \in \dlp{P}^M, A \isect M' = \emptyset,
2186: B \subseteq M \} \union \mbox{}
2187: \end{array}
2188: \\
2189: \{a \IF B \in \nlp{P}^M \mid \begin{array}[t]{@{}l@{}}
2190: a \in M, B \subseteq M \} \union \mbox{}
2191: \end{array}
2192: \\
2193: \{f \IF M \} .
2194: \end{array}
2195: \]
2196: %
2197: It is easy to check that (i)~$N$ is a model of
2198: $\GLred{\test{P}{M}}{N}$.
2199: Assume there is a model $N'$ of $\GLred{\test{P}{M}}{N}$
2200: such that $N' \subseteq N$ holds.
2201: We show that then (ii)~$N \subseteq N'$ holds
2202: as follows. We notice that for all $a \in
2203: \hb{P}$, $a \in N'$ implies $a\in M'$.
2204: %
2205: Consider $A \IF B \in \GLred{P}{M}$.
2206: %
2207: If $B$ is true in $N'\isect\hb{P}$, then $B$ is true in $M'$ and, thus,
2208: $B \subseteq M$ and some $a \in A\isect M\isect M'$. Then $a \IF B \in
2209: \GLred{\test{P}{M}}{N}$ and $a \in N'$. Hence, $N'\isect\hb{P}$ is a
2210: model of $\GLred{P}{M}$ which implies $M' \subseteq N'\isect\hb{P}$.
2211: If $\hat{a} \in N$, then $a \not\in M'$ and $\hat{a} \IF
2212: \in \GLred{\test{P}{M}}{N}$ implying $\hat{a} \in N'$.
2213: Then $N \subseteq N'$ holds.
2214: Now (i) and (ii) imply that $N$ is a minimal model
2215: of $\GLred{\test{P}{M}}{N}$ and, hence, a
2216: stable model of $\test{P}{M}$.
2217: \end{proof}
2218:
2219: \begin{example}
2220: Consider a disjunctive program $P$ and its generator $\gen{P}$:
2221: %
2222: \[
2223: \begin{array}{l}
2224: P =
2225: \begin{array}[t]{l}
2226: \{a \lor b \IF \naf c\}
2227: \end{array}
2228: \\
2229: \\
2230: \gen{P}= \{
2231: \begin{array}[t]{@{\,}l}
2232: a \IF \naf \hat{a},\naf c\END
2233: b \IF \naf \hat{b},\naf c\END \\
2234: \hat{a} \IF \naf a\END \hat{b} \IF \naf b\END
2235: \\
2236: f \IF \naf f, \naf a, \naf b, \naf c \END \\
2237: \supp{a} \IF \naf b, \naf c \END
2238: \supp{b} \IF \naf a, \naf c \END \\
2239: f \IF \naf f, a, \naf \supp{a} \END
2240: f \IF \naf f, b, \naf \supp{b}
2241: \; \}
2242: \end{array}
2243: \end{array}
2244: \]
2245: %
2246: For a stable model $\{b, \supp{b}, \hat{a}\}$ of
2247: $\gen{P}$ the corresponding model candidate is $M_1=\{b, \supp{b}, \hat{a}\}
2248: \isect \hb{P} = \{b\} $ and the test program:
2249: %
2250: \[
2251: \begin{array}[t]{l@{\,}l}
2252: \test{P}{M_1} = \{
2253: & b \IF \naf \hat{b}\END \\
2254: & \hat{a} \IF \naf a\END \hat{b} \IF \naf b\END \\
2255: & f \IF \naf f, \naf a, \naf b \END
2256: f \IF \naf f, b
2257: \; \}
2258: \end{array}
2259: \]
2260: %
2261: $\test{P}{M_1}$ has no stable models and, hence, $M_1$ is a stable model
2262: of $P$.
2263: %
2264: \ebox
2265: \end{example}
2266: %
2267: The simple generate and test paradigm can be optimized by building
2268: model candidates gradually. This means that we start from the empty
2269: partial interpretation and extend the interpretation step by step. An
2270: interesting observation is that the technique for testing minimality
2271: can be used to rule out a partial model candidate of $\gen{P}$ at any
2272: stage of the search and not just when a total model of the program $P$
2273: has been found. This can be done by treating a partial interpretation
2274: $M$ as a total interpretation where undefined atoms are taken to be
2275: false and using the $\test{P}{M}$ program.
2276:
2277: \begin{proposition}
2278: \label{prop:early-test}
2279: %
2280: Let $P$ be a disjunctive program and $M$ a total interpretation. If
2281: $\test{P}{M}$ has a stable model, then there is no (total) stable
2282: model $M'$ of $P$ such that $M \subseteq M'$.
2283: \end{proposition}
2284:
2285: \begin{proof}
2286: Let $\test{P}{M}$ have a stable model. As shown in the proof of
2287: Proposition~\ref{prop:mintest}, then there is a model $M''$ of
2288: $\GLred{P}{M}$ with $M'' \subset M$.
2289: %
2290: Consider any total interpretation $M'$ such that $M \subseteq M'$ and
2291: $M'$ is a model of $\GLred{P}{M'}$.
2292: %
2293: Now $M'$ is not a minimal model of $\GLred{P}{M'}$ as
2294: $\GLred{P}{M'}\subseteq \GLred{P}{M}$ and, hence, $M''$ is a model of
2295: $\GLred{P}{M'}$ but $M'' \subset M \subseteq M'$.
2296: \end{proof}
2297:
2298: Notice that for a total interpretation $M$,
2299: Proposition~\ref{prop:early-test} can only be used for eliminating
2300: stable models of $P$ extending $M$. For guaranteeing the existence of
2301: a stable model of $P$, a total model of $P$ needs to be found making
2302: Proposition~\ref{prop:mintest} applicable.
2303:
2304: Our approach to testing minimality of model candidates differs from
2305: that used in \sys{dlv}~\cite{KLP03:aij}. We check minimality by
2306: directly searching for models of the reduct strictly contained in the
2307: candidate model. In \sys{dlv} a dual approach is used based on the
2308: notion of unfounded sets for disjunctive programs~\cite{LRS97:ic} and minimality
2309: testing is done using a SAT solver. Our approach could be implemented
2310: straightforwardly using a SAT solver, too, but we have chosen to use
2311: the same logic program core engine for generating and testing subtasks
2312: in order to keep the implementation as simple as possible. A basic
2313: difference is that in our approach the set of clauses
2314: (\ref{eq:min-test}) used for minimality testing follow the structure
2315: of the original program whereas in the \sys{dlv} approach dual clauses
2316: (with each literal complemented) are employed. Moreover, \sys{dlv}
2317: employs a couple of optimizations which have not been exploited in our
2318: approach. First, \sys{dlv} adopts specialized algorithms for some
2319: syntactically recognizable classes of rules like head cycle free
2320: programs. Second, \sys{dlv} employs modular evaluation techniques for
2321: minimality testing where the program is divided into components based
2322: on its dependency graph and the minimality of a candidate model is
2323: tested for each component separately by exploiting specialized
2324: algorithms for components with corresponding restricted form whenever
2325: possible. For a more detailed comparison, see~\cite{KLP03:aij}.
2326:
2327: %==============================================================================
2328:
2329: \section{EXPERIMENTS}
2330: \label{section:experiments}
2331:
2332: In this section, we compare \sys{dlv}~\cite{DLV}, a state-of-the-art
2333: implementation of the stable model semantics for disjunctive logic
2334: programs, with an implementation of the generate and test approach of
2335: the previous section which we call \sys{GnT}.
2336: In Section~\ref{section:implementation} we explain briefly implementation
2337: techniques employed in \sys{GnT} and
2338: explain the setup for the experiments.
2339: %
2340: For comparisons we use three families of test problems
2341: related to reasoning about {\em minimal models}~\cite{EG95:amai},
2342: evaluating {\em quantified Boolean formulas}~\cite{Stockmeyer77:tcs},
2343: and {\em planning}~\cite{Niemela99:amai} for which
2344: encodings of the problem instances as logic
2345: programs and test results are presented in
2346: Sections~\ref{section:mm}--\ref{section:planning}, respectively.
2347: All benchmarks used in the experiments are available at
2348: \url{http://www.tcs.hut.fi/Software/gnt/benchmarks/jnssy-tests-2003.tgz}.
2349:
2350:
2351: \subsection{IMPLEMENTATION}
2352: \label{section:implementation}
2353:
2354: The implementation of \sys{GnT} \cite{GNT} is based on
2355: \sys{smodels}~\cite{SMODELS,SNS02:aij}, a program that computes stable
2356: models of normal logic programs. The basic idea behind \sys{GnT} is to
2357: use two instances of the
2358: \sys{smodels} engine, one that generates the model candidates and one
2359: that checks if they are minimal. To implement the idea it is enough to
2360: extend the \sys{smodels} engine only slightly. Figure~\ref{fig:gnt}
2361: shows the pseudo-code for \sys{GnT} modified from the original
2362: $\smodels$ function presented in~\cite{SNS02:aij}. The function
2363: $\gnt(\GP,P,A)$ takes as input a normal (generator) program $\GP$, a
2364: disjunctive program $P$ and a partial model (a set of literals) $A$
2365: and performs a backtracking search for stable models of $\GP$. It
2366: returns a stable model $M$ of $\GP$ which agrees with $A$ and for
2367: which $\isminimal(P,M)$ returns true if such a stable model exists and
2368: otherwise it returns false. It uses functions $expand(\GP,A)$,
2369: $\extend(\GP,A)$, $\conflict(\GP,A)$, $\heuristic(\GP,A)$, and
2370: $\isminimal(P,A)$. The first four are as in the original $\smodels$
2371: procedure:
2372: %
2373: \begin{itemize}
2374: \item
2375: %
2376: $\expand(\GP,A)$ returns a partial model which expands the given
2377: partial model $A$ by literals satisfied by all (total) stable models
2378: of $\GP$ agreeing with $A$ (obtained using a generalized well-founded
2379: computation);
2380:
2381: \item
2382: %
2383: $\extend(\GP,A)$ returns a partial model extending the partial model
2384: $A$ by literals obtained by $\expand$ enhanced with lookahead
2385: techniques.
2386:
2387: \item
2388: %
2389: $\conflict(\GP,A)$ checks whether there is an immediate conflict,
2390: i.e., if the partial model $A$ contains a complementary pair of
2391: literals and
2392:
2393: \item
2394: %
2395: $\heuristic(\GP,A)$ returns an atom undefined in $A$ to be used as the
2396: next choice point in the backtracking search for stable models.
2397: \end{itemize}
2398: %
2399: For further details on these functions see~\cite{SNS02:aij}. The
2400: function $\isminimal(P,A)$ performs the minimality test for a
2401: disjunctive program $P$ and a partial model $A$ given in
2402: Proposition~\ref{prop:early-test} using a call to \sys{smodels}, i.e.,
2403: it views $A$ as a total model $A'$ where all atoms undefined in $A$
2404: are taken to be false, builds the program $\test{P}{A'}$, calls
2405: \sys{smodels} and returns false if $\test{P}{A'}$ has a stable model
2406: and otherwise returns true. To compute a stable model for a
2407: disjunctive program $P$, the procedure $\gnt(\gen{P},P,\emptyset)$ is
2408: called. First $\gnt$ extends the given partial model and checks for
2409: conflicts. If all atoms are covered by the extended partial model,
2410: then a (total) model candidate has been found and it is checked for
2411: minimality. Otherwise the heuristic function selects a new undefined
2412: atom $x$ and $\gnt$ searches recursively first for models where $x$ is
2413: false. If no such model is found, the partial model is expanded by
2414: making $x$ true. If there is a conflict or the expanded model does not
2415: pass an ``early'' minimality test, the procedure backtracks and
2416: otherwise it continues the search recursively using the expanded
2417: model. As the ``early'' minimality tests are computationally quite
2418: expensive, some optimization has been employed so that
2419: such tests are performed only when backtracking from
2420: a model candidate. For this there is a global
2421: variable 'WasCovered' which is initially set to false and which is set
2422: to true when a model candidate is found.
2423: However, it should be noticed that when backtracking from a model
2424: candidate, the test could be repeated at each backtracking level until
2425: it succeeds.
2426: %
2427: The implementation of the $\gnt$ procedure shown in Figure
2428: \ref{fig:gnt} consists of a few hundred lines of code~\cite{GNT} on
2429: top of the \sys{smodels} system.
2430:
2431: \begin{figure}
2432: \begin{tabbing}
2433: xx\=xx\=xx\=xx\=xx\=xx\=xx\=\kill
2434: \textbf{function} $\gnt(\GP,P,A)$ \\
2435: $A:=\extend(\GP,A)$ \\
2436: \keyw{if} {$\conflict(\GP,A)$} \keyw{then} \\
2437: \> return false \\
2438: \keyw{else if} {$A$ covers $\hb{\GP}$} \keyw{then} \\
2439: \> WasCovered := true \\
2440: \> \keyw{if} {$\isminimal(P,A)$ } \keyw{then} \\
2441: \> \> return $A$ \\
2442: \> \keyw{else} \\
2443: \> \> return false \\
2444: \> \keyw{end if} \\
2445: \keyw{else}\\
2446: \> $x:=\heuristic(\GP,A)$\\
2447: \> $A'$ := $\gnt(\GP,P,A\cup \{\naf x\})$ \\
2448: \> \keyw{if} $A' \not= false$ \keyw{then} \\
2449: \>\> return $A'$ \\
2450: \> \keyw{else} \\
2451: \>\> $A' := \expand(\GP,A\cup \{x\})$ \\
2452: \>\> \keyw{if} $\conflict(\GP,A')$ \keyw{then} \\
2453: \>\>\> return false \\
2454: \>\> \keyw{else if} WasCovered \keyw{then} \\
2455: \>\>\> \keyw{if} not $\isminimal(P,A')$ \keyw{then} \\
2456: \>\>\>\> return false \\
2457: \>\>\> \keyw{end if}\\
2458: \>\> \keyw{end if} \\
2459: \>\> WasCovered := false \\
2460: \>\> return $\gnt\bigl(\GP,P,A'\bigr)$\\
2461: \> \keyw{end if}\\
2462: \keyw{end if}.
2463: \end{tabbing}
2464: \caption{\sys{GnT} Procedure}
2465: \label{fig:gnt}
2466: \end{figure}
2467:
2468: In the sequel, we report several experiments which we carry out in
2469: order to compare \sys{dlv} (version 2003-05-16) with \sys{GnT}
2470: which is based on \sys{smodels} (version 2.27) and
2471: uses \sys{lparse} (version 1.0.13) as an instantiator.
2472: We consider two versions
2473: of our approach, \sys{GnT1} and \sys{GnT2}, which are similar except
2474: that in \sys{GnT1} generating program $\genI{P}$ is used and in
2475: \sys{GnT2}, $\gen{P} =\genI{P} \cup \support{P}$.
2476: %
2477: All of our tests are run under Linux 2.4.20 operating system on a
2478: 1.7 GHz AMD Athlon XP 2000+ computer with $1$ GB of memory. Execution
2479: times are measured using the customary Unix \texttt{/usr/bin/time}
2480: command.
2481:
2482: \subsection{MINIMAL MODELS}
2483: \label{section:mm}
2484:
2485: Our first test problem is the $\Sigma^p_2$-complete problem of
2486: deciding the existence of a minimal model of a set of clauses in which
2487: some specified atoms are true \cite{EG95:amai}.
2488: %
2489: This problem is mapped to a stable model computation problem as
2490: follows. For a problem instance consisting of a set of clauses and
2491: some specified atoms, a program $P$ is constructed where each clause
2492: $a_1\lor\dotsb\lor a_n\lor\neg b_1\lor\dotsb\lor \neg b_m$ is
2493: translated into a rule $a_1\lor\dotsb\lor a_n \IF b_1,\dotsc,b_m$ and
2494: for each specified atom $c_i$, a rule
2495: %
2496: \begin{equation}
2497: f\IF\naf f,\naf c_i\qquad
2498: \label{eq:true-atoms}
2499: \end{equation}
2500: %
2501: is included. Now $P$ has a stable model if and only if there is a
2502: minimal model of the clauses containing all specified atoms $c_i$.
2503:
2504: The test cases (random disjunctive 3-SAT programs) are based on random
2505: 3-SAT problems having a fixed clauses/atoms ratio $c$ and they are
2506: constructed as follows. Given a number of atoms $n$, a random 3-SAT
2507: problem is generated, i.e.\ $c\times n$ clauses are generated each by
2508: picking randomly three distinct atoms from the $n$ available and
2509: selecting their polarity uniformly. This is done using a program
2510: \sys{makewff} developed by Bart Selman. Then the clauses are
2511: translated into rules as described above and for $i=1,\dotsc,\lfloor
2512: 2n/100\rfloor$ and for random atoms $c_i$, the extra rules
2513: (\ref{eq:true-atoms}) are added.
2514: %
2515: The problem size is controlled by the number of atoms $n$ which is
2516: increased by increments of $10$. For each $n$, we test $100$ random
2517: 3-SAT programs and measure the maximum, average, and minimum time it
2518: takes to decide whether a stable model exists.
2519:
2520: In the first set of tests we study the effect of different generating
2521: programs on the performance of our approach, i.e., we compare
2522: \sys{GnT1} and \sys{GnT2}, which are similar except
2523: that in \sys{GnT1} generating program $\genI{P}$ is used and in
2524: \sys{GnT2}, $\gen{P} =\genI{P} \cup \support{P}$. We test at two
2525: clauses/atoms ratios. The first test is at 4.258 which is in the
2526: phase transition region~\cite{CA96:aij} where roughly 50\% of the
2527: generated 3-SAT clause sets are satisfiable. The second test is at
2528: clauses/atoms ratio 3.750 where practically all generated 3-SAT clause
2529: sets are satisfiable.
2530:
2531: The test results are shown in Figure~\ref{fig:expI}. In the first test
2532: set the key problem seems to be finding at least one model candidate.
2533: The simpler generator (\sys{GnT1}) appears to perform relatively well except
2534: for a few outliers, i.e.\ instances with significantly higher running
2535: time than the average. The outliers occur when the generator program
2536: $\genI{P}$ allows a high number of candidate models. At clauses/atoms
2537: ratio 3.750 the frequency of outliers for \sys{GnT1} increases and outliers
2538: occur already in smaller problem sizes. The more involved generating
2539: program $\gen{P}$ behaves in a much more robust way and the average
2540: running time of \sys{GnT2} is significantly lower than that of \sys{GnT1}.
2541: %
2542: Next we use the same two test sets for comparing \sys{GnT2} and
2543: \sys{dlv}. The results are shown in Figure~\ref{fig:expII}. The
2544: systems scale very similarly in both test sets but \sys{dlv} seems to
2545: be roughly a constant factor faster than \sys{GnT2}. This is probably
2546: due to the overhead caused by the more complicated generating program
2547: in \sys{GnT2} and by the two level architecture of \sys{GnT2} where
2548: two instances of \sys{smodels} are cooperating.
2549:
2550: \begin{figure*}
2551: \begin{center}
2552: \begin{tabular}{c}
2553: \includegraphics{experiment-gnt1-vs-gnt2-4.258.1.ps} \\
2554: \ \\
2555: \ \\
2556: \includegraphics{experiment-gnt1-vs-gnt2-3.750.1.ps}
2557: \end{tabular}
2558: \caption{Minimal Models: \sys{GnT1} vs.\ \sys{GnT2}}
2559: \label{fig:expI}
2560: \end{center}
2561: \end{figure*}
2562:
2563: \begin{figure*}
2564: \begin{center}
2565: \begin{tabular}{c}
2566: \includegraphics{experiment-dlv-vs-gnt2-4.258.1.ps} \\
2567: \ \\
2568: \ \\
2569: \includegraphics{experiment-dlv-vs-gnt2-3.750.1.ps}
2570: \end{tabular}
2571: \caption{Minimal Models: \sys{dlv} vs.\ \sys{GnT2}}
2572: \label{fig:expII}
2573: \end{center}
2574: \end{figure*}
2575:
2576: \subsection{QUANTIFIED BOOLEAN FORMULAS}
2577:
2578:
2579: We continue the comparison of \sys{GnT2} and \sys{dlv} using instances
2580: of quantified Boolean formulas (QBFs) and develop a new way to encode
2581: such formulas as disjunctive logic programs. In our experiments, we
2582: consider a specific subclass of QBFs, namely $2,\exists$-QBFs. Such
2583: formulas are of the form $\exists X\forall Y\phi$ where $X$ and $Y$
2584: are sets of existentially and universally quantified propositional
2585: variables, respectively, and $\phi$ is a Boolean formula based on
2586: $X\union Y$.
2587: %
2588: Deciding the validity of such a formula forms a $\Sigma^p_2$-complete
2589: decision problem \cite{Stockmeyer77:tcs} even if $\phi$ is assumed to
2590: be a Boolean formula in 3DNF \cite{SM73:stoc}. Recall that checking
2591: the existence of a stable model for a disjunctive logic program is of
2592: equal computational complexity \cite{EG95:amai}, which implies the
2593: existence of polynomial time transformations between the decision
2594: problems mentioned above.
2595: %
2596: In fact, Eiter and Gottlob \cite{EG95:amai} show how a QBF of the form
2597: $\exists X\forall Y\phi$ with $\phi$ in 3DNF can be translated into
2598: a disjunctive logic program $P$ such that $\exists X\forall Y\phi$ is
2599: valid if and only if $P$ has a stable model. This translation is used
2600: by Leone et al.~\cite{LPFEGPS03:submitted} to compare \sys{dlv} and
2601: \sys{GnT2}.
2602:
2603: However, we present an alternative transformation in order to obtain a
2604: better performance for the two systems under comparison. Our
2605: transformation is based on the following ideas. The first observation
2606: is that we can rewrite $\exists X\forall Y\phi$ with $\phi$ in DNF as
2607: $\exists X\neg\exists Y\neg\phi$ where $\neg\phi$ can be understood as
2608: a Boolean formula in CNF or as a {\em set of clauses} $S$ so that each
2609: clause $c\in S$ can represented as a disjunction of the form
2610: %
2611: \begin{equation}
2612: \label{eq:clause}
2613: X_1\lor\neg X_2\lor Y_1\lor\neg Y_2
2614: \end{equation}
2615: %
2616: where $X_1$ and $\neg X_2$ are the sets of positive and negative
2617: literals, respectively, which appear in $c$ and involve variables from
2618: $X$ while $Y_1$ and $\neg Y_2$ are similarly related to $Y$.
2619: %
2620: It follows that $\exists X\forall Y\phi$ is valid if and only if we
2621: can find an interpretation\footnote{The values assigned by $I$ to the
2622: variables in $Y$ are not important, but make $I$ a proper
2623: interpretation over $X\union Y$.} $\func{I}{X\union
2624: Y}{\set{\true,\false}}$ such that $\neg\phi_{I(X)}$ is unsatisfiable
2625: where $\neg\phi_{I(X)}$ denotes the set of clauses $Y_1\lor\neg Y_2$
2626: for which (\ref{eq:clause}) belongs to $S$ and $I\not\models
2627: X_1\lor\neg X_2$.
2628: %
2629: The second idea behind our transformation is to choose the truth value
2630: of the condition $X_1\lor\neg X_2$ for each clause (\ref{eq:clause})
2631: in $S$ rather than the truth values of the variables in $X\union Y$.
2632: %
2633: This line of thinking leads to the following translation of $S$.
2634:
2635: \begin{definition}
2636: \label{def:QBF-transformation}
2637: A clause $c$ of the form (\ref{eq:clause}) where $X_1,X_2\subseteq X$
2638: and $Y_1,Y_2\subseteq Y$ is translated into following sets of rules:
2639: %
2640: \begin{center}
2641: $\begin{array}{r@{\ }c@{\ }l}
2642: \tr{V}{c} & = & \set{c\IF\naf\hat{c}\END
2643: \hat{c}\IF\naf c}, \\
2644: \tr{E}{c} & = & \sel{f\IF x,\naf\hat{c},\naf f}{x\in X_1}\union
2645: \sel{x\IF\naf\hat{c}}{x\in X_2}\ \union \\
2646: & & \set{f\IF X_2,\naf X_1,\naf c,\naf f},\text{ and} \\
2647: \tr{U}{c} & = & \sel{y\IF u}{y\in Y_1\union Y_2}\union
2648: \set{Y_1\union\set{u}\IF Y_2,\naf \hat{c}}
2649: \end{array}$
2650: \end{center}
2651: %
2652: where $c$ and $\hat{c}$ are new atoms associated with the clause $c$,
2653: and $f$ and $u$ are new atoms. A set of clauses $S$ is translated into
2654: %
2655: \begin{center}
2656: $\Union_{c\in S}(\tr{V}{c}\union\tr{E}{c}\union\tr{U}{c})
2657: \union\set{u\IF\naf u}$.
2658: \end{center}
2659: \end{definition}
2660:
2661: We use Boolean variables from $X\union Y$ as propositional atoms in
2662: the translation.
2663: %
2664: Intuitively, the rules of $\tr{V}{c}$ choose whether a clause $c$ is
2665: {\em active}, i.e.\ $X_1\lor\neg X_2$ evaluates to false so that the
2666: satisfaction of the clause $c$ depends on the values assigned to
2667: $Y_1\union Y_2$. The rules in $\tr{E}{c}$ try to {\em explain} the
2668: preceding choice by checking that the values of the variables in $X$
2669: can be assigned accordingly. Finally, the rules in $\tr{U}{c}$
2670: implement the test for unsatisfiability together with the rule
2671: $u\IF\naf u$.
2672: %
2673: Basically, the same unsatisfiability check is used in the translation
2674: proposed by Eiter and Gottlob. However, the transformation given in
2675: Definition \ref{def:QBF-transformation} is more economical as it uses
2676: far less new atoms and disjunctive rules. In particular, note that
2677: variables from $X\union Y$ not appearing in the clauses do not
2678: contribute any rules to the translation.
2679:
2680: Next we address the correctness of our transformation and consider a
2681: $2,\exists$-QBF $\exists X\forall Y\phi$ where $\phi$ is in DNF and
2682: the disjunctive logic program $P$ obtained by translating $\neg\phi$
2683: (a set of clauses $S$) according to Definition
2684: \ref{def:QBF-transformation}.
2685:
2686: \begin{lemma}
2687: \label{lemma:reduct}
2688: Let $M\subseteq\hb{P}$ be a total propositional interpretation for the
2689: translation $P$ such that for every clause $c\in S$ of the form
2690: (\ref{eq:clause}), (i) $c\in M$ $\iff$ $\hat{c}\not\in M$ and (ii)
2691: $c\in M$ $\iff$ $X_1\isect M=\emptyset$ and $X_2\subseteq M$.
2692:
2693: Then the programs $\tr{V}{c}$,
2694: $\tr{E}{c}$, and $\tr{U}{c}$ associated with a clause $c\in S$ of the
2695: form (\ref{eq:clause}) satisfy the following.
2696: %
2697: \begin{enumerate}
2698: \item[(R1)]
2699: %
2700: The fact $c\IF$ belongs to $\GLred{\tr{V}{c}}{M}$ $\iff$ $c\in M$.
2701:
2702: \item[(R2)]
2703: %
2704: The fact $\hat{c}\IF$ belongs to $\GLred{\tr{V}{c}}{M}$ $\iff$
2705: $\hat{c}\in M$.
2706:
2707: \item[(R3)]
2708: %
2709: For $x\in X_1$, the rule $f\IF x$ belongs to $\GLred{\tr{E}{c}}{M}$ $\iff$ \\
2710: $x\not\in M$ and $f\not\in M$.
2711:
2712: \item[(R4)]
2713: %
2714: For $x\in X_2$, the fact $x\IF$ belongs to
2715: $\GLred{\tr{E}{c}}{M}$ $\iff$ $x\in M$.
2716:
2717: \item[(R5)]
2718: %
2719: The rule $f\IF X_2$ belongs to
2720: $\GLred{\tr{E}{c}}{M}$ $\iff$ $X_2\not\subseteq M$ and $f\not\in M$.
2721:
2722: \item[(R6)]
2723: %
2724: For $y\in Y_1\union Y_2$, the rule $y\IF u$ belongs to
2725: $\GLred{\tr{U}{c}}{M}$ unconditionally.
2726:
2727: \item[(R7)]
2728: %
2729: The rule $Y_1\union\set{u}\IF Y_2$ belongs to $\GLred{\tr{U}{c}}{M}$
2730: $\iff$ $c\in M$.
2731: \end{enumerate}
2732: \end{lemma}
2733:
2734: \begin{theorem}
2735: The quantified Boolean formula $\exists X\forall Y\phi$ is valid if
2736: and only if the translation $P$ has a stable model.
2737: \end{theorem}
2738:
2739: \begin{proof}
2740: We may safely assume that all variables in $X\union Y$ actually appear
2741: in $\phi$, since redundant variables can be dropped without affecting
2742: the validity of the formula nor the structure of its translation.
2743:
2744: ($\implies$)
2745: %
2746: Suppose that $\exists X\forall Y\phi$ is valid. Then there is an
2747: interpretation $\func{I}{X\union Y}{\set{\true,\false}}$ such that
2748: $I\models\forall Y\phi$.
2749: %
2750: Then define $X_I=\sel{x\in X}{I(x)=\true}$.
2751: %
2752: Without loss of generality we may assume that $X_I$ is minimal, i.e.\
2753: there is no interpretation $J$ such that $J\models\forall Y\phi$ and
2754: $X_J\subset X_I$. Then define a total propositional interpretation
2755: %
2756: \begin{multline}
2757: \label{eq:stable-model-structure}
2758: M=X_I\union Y\union\set{u}\ \union \\
2759: \sel{c}{c=X_1\lor\neg X_2\lor Y_1\lor\neg Y_2\in\neg\phi
2760: \text{ and }I\not\models X_1\lor\neg X_2}\ \union \\
2761: \sel{\hat{c}}{c=X_1\lor\neg X_2\lor Y_1\lor\neg Y_2\in\neg\phi
2762: \text{ and }I\models X_1\lor\neg X_2}.
2763: \end{multline}
2764: %
2765: It is verified next that $M$ is a stable model of $P$. The definition
2766: of $M$ implies that $M$ satisfies the requirements of Lemma
2767: \ref{lemma:reduct}. Then (R1)--(R7) effectively describe the
2768: structure of $\GLred{P}{M}$ and it is easy to verify that $M$ is a
2769: model of $\GLred{P}{M}$ on the basis of these relationships, as
2770: $Y\union\set{u}\subseteq M$ and $f\not\in M$ by definition.
2771:
2772: Next we assume that $N\subseteq M$ is a model of $\GLred{P}{M}$
2773: and show that $M\subseteq N$.
2774: %
2775: (i)
2776: %
2777: If $c\in M$ for some clause $c$ of the form (\ref{eq:clause}),
2778: then $c\in N$, as $c\IF$ belongs to $\GLred{P}{M}$ by (R1).
2779: %
2780: (ii)
2781: %
2782: Similarly, $\hat{c}\in M$ implies $\hat{c}\in N$ by (R2).
2783: %
2784: (iii)
2785: %
2786: We have $u\in N$ because otherwise $N$ would form a model of
2787: $\neg\phi_{I(X)}$ by satisfying the rules $Y_1\union\set{u}\IF Y_2$
2788: included in $\GLred{P}{M}$ by (R7).
2789: %
2790: (iv)
2791: %
2792: Moreover, $Y\subseteq N$ holds, as $u\in N$ and $N$ satisfies all the
2793: rules $y\IF u$ belonging to $\GLred{P}{M}$ by (R6).
2794: %
2795: (v)
2796: %
2797: Let us define an interpretation $\func{J}{X\union
2798: Y}{\set{\true,\false}}$ such that for $x'\in X$, $J(x')=\true$ $\iff$
2799: $x'\in N$, and for $y\in Y$, $J(y)=I(y)$. Using (R4), we can establish
2800: for any (\ref{eq:clause}) that $I\not\models X_1\lor\neg X_2$ implies
2801: $J\not\models X_1\lor\neg X_2$. Thus
2802: $\neg\phi_{I(X)}\subseteq\neg\phi_{J(X)}$ where $\neg\phi_{I(X)}$ is
2803: known to be unsatisfiable. The same follows for $\neg\phi_{J(X)}$ so
2804: that $J$ qualifies as an assignment for which $J\models\forall Y\phi$
2805: holds. But then the minimality of $I$ implies $J=I$, $X_J=X_I$, and
2806: $X_I\subseteq N$.
2807: %
2808: To conclude the preceding analysis,
2809: $M\subseteq N$ and $M$ is a stable model of $P$.
2810:
2811: ($\impliedby$)
2812: %
2813: Suppose that $P$ has a stable model $M$.
2814: %
2815: Then define an interpretation $\func{I}{X\union
2816: Y}{\set{\true,\false}}$ by setting $I(z)=\true$ $\iff$ $z\in M$ for
2817: any $z\in X\union Y$. Let us then establish that $M$ and $I$
2818: satisfy (\ref{eq:stable-model-structure}).
2819: %
2820: (i)
2821: %
2822: The definition of $I$ implies that $X_I=M\isect X$.
2823: %
2824: (ii)
2825: %
2826: Now $u\in M$, because $P$ contains $u\IF\naf u$ and
2827: $M$ is a stable model of $P$.
2828: %
2829: (iii)
2830: %
2831: For the same reason, $f\not\in M$, because all the rules having
2832: $f$ as the head have $\naf f$ among the negative body literals.
2833: %
2834: (iv)
2835: %
2836: Since $u\in M$ and $\GLred{P}{M}$ contains the rule $y\IF u$ for every
2837: $y\in Y$, we obtain $Y\subseteq M$.
2838: %
2839: (v)
2840: %
2841: For any clause $c$ of the form (\ref{eq:clause}), the structure of
2842: $\tr{V}{c}\subseteq P$ implies that $c\in M$ $\iff$ $c\IF$ belongs to
2843: $\GLred{\tr{V}{c}}{M}\subseteq\GLred{P}{M}$ $\iff$ $\hat{c}\not\in M$.
2844: Using this property, we can establish that $c\in M$ $\iff$
2845: $I\not\models X_1\lor\neg X_2$ holds for the interpretation $I$
2846: defined above.
2847: %
2848: (vi)
2849: %
2850: Thus $\hat{c}\in M$ $\iff$ $I\models X_1\lor\neg X_2$ is implied by
2851: the fact that $c\in M$ $\iff$ $\hat{c}\not\in M$, as shown above in (v).
2852:
2853: It remains to show that $\neg\phi_{I(X)}$ is unsatisfiable. So let us
2854: assume the contrary, i.e.\ there is a model $Y'\subseteq Y$ for
2855: $\neg\phi_{I(X)}$. Note that $M$ meets the requirements of Lemma
2856: \ref{lemma:reduct} by (v) and (vi) above, as the definition of $I$
2857: implies $I\not\models X_1\lor\neg X_2$ $\iff$ $X_1\isect M=\emptyset$
2858: and $X_2\subseteq M$.
2859: %
2860: The relationships (R1)--(R7) imply that $N=(M-(Y\union\set{u}))\union
2861: Y'$ is a model of $\GLred{P}{M}$, too. Since $u\not\in N$, we have
2862: $N\subset M$ indicating that $M$ is not stable, a contradiction. Thus
2863: $\neg\phi_{I(x)}$ is unsatisfiable which implies $I\models\forall
2864: Y\phi$ and the validity of $\exists X\forall Y\phi$.
2865: \end{proof}
2866:
2867: Using an implementation of the translation given in Definition
2868: \ref{def:QBF-transformation} we are able to transform $2,\exists$-QBFs
2869: into disjunctive programs. The remaining question is how to generate
2870: $2,\exists$-QBF instances. We use two different schemes based on
2871: random instances \cite{CGS98:aaai,GW99:aaai}.
2872: %
2873: In the first scheme, the sets of variables $X$ and $Y$ satisfy
2874: $|X|=|Y|$. Each random instance is based on $v=|X|+|Y|$ variables and
2875: a Boolean formula $\phi$ which is a disjunction of $d=2\times v$
2876: conjunctions of $5$ random literals out of which at least two literals
2877: involve a variable from $Y$, as suggested by Gent and Walsh
2878: \cite{GW99:aaai}. This scheme is slightly different from
2879: $\mathrm{2QBF}_{GW}$ in \cite{LPFEGPS03:submitted} based on $3$
2880: literal conjunctions just to obtain a more challenging
2881: benchmark.
2882: %
2883: The constant factor $2$ in the equation relating $d$ and $v$ has been
2884: determined as a phase transition point for the \sys{dlv} system by
2885: keeping $v=50$ fixed and varying the number of disjunctions in
2886: $\phi$. In the actual experiment, the number of $v$ variables is
2887: varied from $5$ to $50$ by increments of $5$.
2888: %
2889: We generate $100$ instances of $2,\exists$-QBFs for each value of $v$
2890: and translate them into corresponding disjunctive logic programs. The
2891: running times for \sys{dlv} and $\sys{GnT2}$ are depicted in the upper
2892: graph of Figure \ref{fig:expIII}. The systems scale very similarly,
2893: but \sys{dlv} is on the average from one to two decades faster than
2894: \sys{GnT2}.
2895:
2896: In the second experiment with $2,\exists$-QBFs, we use a different
2897: scheme for the number of disjunctions $d=\lfloor\sqrt{v/2}\rfloor$ as
2898: well as the number of literals which is $3$ in each conjunction. The
2899: resulting instances are much easier to solve, because $d$ remains
2900: relatively low (e.g.\ $d\approx 41$ for $v=3500$) and many variables
2901: do not appear in $\phi$ at all. We let $v$ vary from $50$ to $3550$ by
2902: increments of $50$ and generate $100$ instances of $2,\exists$-QBFs
2903: for each value of $v$. The resulting running times are shown in the
2904: lower graph of Figure \ref{fig:expIII}. The shapes of the curves are
2905: basically the same, but the performance of \sys{GnT2} degrades faster
2906: than that of \sys{dlv}.
2907: %
2908: However, the benefits of the translation given in Definition
2909: \ref{def:QBF-transformation} are clear, as \sys{GnT2} is able to solve
2910: much larger instances than reported in \cite{LPFEGPS03:submitted}
2911: where $40$ variables turn out to be too much for \sys{GnT2}. As far
2912: as we understand, this is due to the sizes of search spaces associated
2913: with the translated instances of $2,\exists$-QBFs. For the translation
2914: given in Definition \ref{def:QBF-transformation}, the size of the
2915: search space examined by \sys{GnT2} is of order $2^{\sqrt{v/2}}$
2916: whereas it is of order $2^v$ if the translation proposed by Eiter and
2917: Gottlob \cite{EG95:amai} is used.
2918:
2919: \begin{figure*}
2920: \begin{center}
2921: \begin{tabular}{c}
2922: \includegraphics{experiment-dlv-vs-gnt2-qbf.ps} \\
2923: \ \\
2924: \ \\
2925: \includegraphics{experiment-dlv-vs-gnt2-qbf-sqrt.ps}
2926: \end{tabular}
2927: \end{center}
2928: \caption{Quantified Boolean Formulas: \sys{dlv} vs.\ \sys{GnT2}}
2929: \label{fig:expIII}
2930: \end{figure*}
2931:
2932: \subsection{PLANNING}
2933: \label{section:planning}
2934:
2935: In order to get an idea of the overhead of \sys{GnT2} when compared to
2936: \sys{smodels}, we study three blocks world planning problems encoded
2937: as normal programs~\cite{Niemela99:amai}:
2938: %
2939: \begin{itemize}
2940: \item
2941: %
2942: {large.c} is a 15 blocks problem requiring a 8 step plan using the
2943: encoding given in~\cite{Niemela99:amai} allowing parallel execution of
2944: operators,
2945:
2946: \item
2947: %
2948: {large.d} is a 17 blocks problem with a 9 step plan and
2949:
2950: \item
2951: %
2952: {large.e} is a 19 blocks problem with a 10 step plan.
2953: \end{itemize}
2954: %
2955: Table~\ref{table:bw-results} contains two entries for each problem:
2956: one reporting the time needed to find a valid plan with the
2957: ``optimal'' number of steps given as input and one reporting the time
2958: needed to show optimality, i.e., that no plan (no stable model) exists
2959: when the number of situations is decreased by one. The times reported
2960: for each test case are the execution times of \sys{smodels} and
2961: \sys{GnT2} given a ground normal program (generated by \sys{lparse})
2962: as input. The results show that there is some overhead in the current
2963: implementation of \sys{GnT2} even for normal programs and \sys{GnT2}
2964: handles these examples 2-4 times slower than \sys{smodels}.
2965:
2966: \begin{table}
2967: \centering
2968: \caption{Planning: \sys{smodels} vs.\ \sys{GnT2}}
2969: \label{table:bw-results}
2970:
2971: \begin{tabular}{lrrrr} \hline
2972: Problem & Number of & Number of & Time (s) & Time (s)\\
2973: & steps & ground rules & \sys{smodels} & \sys{GnT2} \\ \hline
2974: large.c & 8 & 81681 & 4.5 & 10.3 \\
2975: & 7 & 72527 & 0.6 & 2.1 \\ \hline
2976: large.d & 9 & 127999 & 10.1 & 21.2 \\
2977: & 8 & 115109 & 1.4 & 5.2\\ \hline
2978: large.e & 10 & 191621 & 18.2 & 35.0\\
2979: & 9 & 174099 & 2.2 & 8.7\\ \hline
2980: \end{tabular}
2981: \end{table}
2982:
2983: %==============================================================================
2984:
2985: \section{CONCLUSIONS}
2986: \label{section:conclusions}
2987:
2988: The paper presents an approach to implementing partial and disjunctive
2989: stable models using an implementation of stable models for
2990: disjunction-free programs as the core inference engine. The approach
2991: is based on unfolding partiality and disjunctions from a logic program
2992: in two separate steps. In the first step partial stable models of
2993: disjunctive programs are captured by total stable models using a
2994: simple linear program transformation. Thus, reasoning tasks
2995: concerning partial models can be solved using an implementation of
2996: total models such as the \sys{dlv} system. This also sheds new light
2997: on the relationship between partial and total stable models by
2998: establishing a close correspondence. In the second step a generate
2999: and test approach is developed for computing total stable models of
3000: disjunctive programs using a core engine capable of computing stable
3001: models of normal programs. We have developed an implementation of the
3002: approach using \sys{smodels} as the core engine. The extension is
3003: fairly simple consisting of a few hundred lines of code. The approach
3004: turns out to be competitive even against a state-of-the-art system for
3005: disjunctive programs. The efficiency of the approach comes partly
3006: from the fact that normal programs can capture essential properties of
3007: disjunctive stable models that help with decreasing the computational
3008: complexity of the generate and test phases in the approach. However, a
3009: major part of the success can be accounted for by the efficiency of
3010: the core engine. This suggests that more efforts should be spent in
3011: developing efficient core engines.
3012:
3013: \subsubsection*{ACKNOWLEDGEMENTS}
3014:
3015: The work of the first, the second and the fourth author has been
3016: funded by the Academy of Finland (projects \#43963 and \#53695), and
3017: that of the fourth author also by the Helsinki Graduate School in
3018: Computer Science and Engineering. We thank Tommi Syrjänen for
3019: implementing the front-end \sys{lparse} for the \sys{smodels}
3020: \cite{SMODELS} system and for incorporating the relevant translations
3021: into the implementation. We also thank Emilia Oikarinen who
3022: implemented the transformation from QBFs to disjunctive programs.
3023:
3024: %==============================================================================
3025:
3026: \renewcommand{\refname}{REFERENCES}
3027:
3028: % !!! Remember to add \sys-macro to certain references for the final v. !!!
3029:
3030: \begin{thebibliography}{10}
3031:
3032: \bibitem{CMODELS}
3033: Y.~Babovich.
3034: \newblock \sys{cmodels} ---
3035: a tool for computing answer sets using {SAT} solvers.
3036: \newblock
3037: \url{http://www.cs.utexas.edu/users/tag/cmodels.html}, 2003.
3038: \newblock Computer Program.
3039:
3040: \bibitem{BBGBW01:padl}
3041: M.~Balduccini, M.~Barry, M.~Gelfond, M.~Nogueira, and R.~Watson.
3042: \newblock An {A-Prolog} decision support system for the space shuttle.
3043: \newblock In {\em Proceedings of the Third International Symposium on Practical
3044: Aspects of Declarative Languages}, Las Vegas, Nevada, 2001. Springer-Verlag.
3045:
3046: \bibitem{BD97:jlp}
3047: S.~Brass and J.~Dix.
3048: \newblock Characterizations of the (disjunctive) stable semantics by partial
3049: evaluation.
3050: \newblock {\em Journal of Logic Programming}, 32(3):207--228, 1997.
3051:
3052: \bibitem{BD99:jlp}
3053: S.~Brass and J.~Dix.
3054: \newblock Semantics of (disjunctive) logic programs based on partial
3055: evaluation.
3056: \newblock {\em Journal of Logic Programming}, 38(3):167--213, 1999.
3057:
3058: \bibitem{BLR97:lpnmr}
3059: F.~Buccafurri, N.~Leone, and P.~Rullo.
3060: \newblock Strong and weak constraints in disjunctive datalog.
3061: \newblock In {\em Proceedings of the 4th International Conference on Logic
3062: Programming and Non-Monotonic Reasoning}, pages 2--17. Springer-Verlag, 1997.
3063:
3064: \bibitem{CGS98:aaai}
3065: M.~Cadoli, A.~Giovanardi, and M.~Schaerf.
3066: \newblock An algorithm to evaluate quantified boolean formulae.
3067: \newblock In {\em Proceedings of the 15th National Conference on Artificial
3068: Intelligence}, pages 262--267, Madison, Wisconsin, USA, July 1998. AAAI, MIT
3069: Press.
3070:
3071: \bibitem{CA96:aij}
3072: J.~Crawford and L.~Auton.
3073: \newblock Experimental results on the crossover point in random 3-{SAT}.
3074: \newblock {\em Artificial Intelligence}, 81(1):31--57, 1996.
3075:
3076: \bibitem{DNK97:planning}
3077: Y.~Dimopoulos, B.~Nebel, and J.~Koehler.
3078: \newblock Encoding planning problems in non-monotonic logic programs.
3079: \newblock In {\em Proceedings of the Fourth European Conference on Planning},
3080: pages 169--181, Toulouse, France, September 1997. Springer-Verlag.
3081:
3082: \bibitem{DGM96:fi}
3083: J.~Dix, G.~Gottlob, and M.~Marek.
3084: \newblock Reducing disjunctive to non-disjunctive semantics by
3085: shift-operations.
3086: \newblock {\em Fundamenta Informaticae}, 28:87--100, 1996.
3087:
3088: \bibitem{Dung95:jlp}
3089: P.~Dung.
3090: \newblock An argumentation theoretic foundation for logic programming.
3091: \newblock {\em Journal of Logic Programming}, 22:151--177, 1995.
3092:
3093: \bibitem{EFLPP2000:cl}
3094: T.~Eiter, W.~Faber, N.~Leone, G.~Pfeifer, and A.~Polleres.
3095: \newblock Planning under incomplete knowledge.
3096: \newblock In {\em Proceedings of the First International Conference on
3097: Computational Logic}, pages 807--821, London, U.K., July 2000.
3098: Springer-Verlag.
3099:
3100: \bibitem{EG95:amai}
3101: T.~Eiter and G.~Gottlob.
3102: \newblock On the computational cost of disjunctive logic programming:
3103: Propositional case.
3104: \newblock {\em Annals of Mathematics and Artificial Intelligence}, 15:289--323,
3105: 1995.
3106:
3107: \bibitem{EGM97:acmtds}
3108: T.~Eiter, G.~Gottlob, and H.~Mannila.
3109: \newblock Disjunctive datalog.
3110: \newblock {\em ACM Transactions on Database Systems}, 22(3):364--418, 1997.
3111:
3112: \bibitem{ELS97:amai}
3113: T.~Eiter, N.~Leone, and D.~Sacc\`{a}.
3114: \newblock On the partial semantics for disjunctive deductive databases.
3115: \newblock {\em Annals of Mathematics and Artificial Intelligence},
3116: 17(1/2):59--96, 1997.
3117:
3118: \bibitem{ELS98:tcs}
3119: T.~Eiter, N.~Leone, and D.~Sacc\`{a}.
3120: \newblock Expressive power and complexity of partial models for disjunctive
3121: deductive databases.
3122: \newblock {\em Theoretical Computer Science}, 206(1/2):181--218, 1998.
3123:
3124: \bibitem{EK89:iclp}
3125: K.~Eshghi and R.~Kowalski.
3126: \newblock Abduction compared with negation by failure.
3127: \newblock In {\em Proceedings of the 6th International Conference on Logic
3128: Programming}, pages 234--254. MIT Press, 1989.
3129:
3130: \bibitem{GL88:iclp}
3131: M.~Gelfond and V.~Lifschitz.
3132: \newblock The stable model semantics for logic programming.
3133: \newblock In {\em Proceedings of the 5th International Conference on Logic
3134: Programming}, pages 1070--1080, Seattle, USA, August 1988. MIT Press.
3135:
3136: \bibitem{GL91:ngc}
3137: M.~Gelfond and V.~Lifschitz.
3138: \newblock Classical negation in logic programs and disjunctive databases.
3139: \newblock {\em New Generation Computing}, 9:365--385, 1991.
3140:
3141: \bibitem{GW99:aaai}
3142: I.~Gent and T.~Walsh.
3143: \newblock Beyond {NP}: The {QSAT} phase transition.
3144: \newblock In {\em {AAAI}: 16th National Conference on Artificial Intelligence},
3145: pages 648--653. AAAI / MIT Press, 1999.
3146:
3147: \bibitem{Heljanko99:fi}
3148: K.~Heljanko.
3149: \newblock Using logic programs with stable model semantics to solve deadlock
3150: and reachability problems for 1-safe {Petri} nets.
3151: \newblock {\em Fundamenta Informaticae}, 37(3):247--268, 1999.
3152:
3153: \bibitem{JNSY00:kr}
3154: T.~Janhunen, I.~Niemelä, P.~Simons, and J.-H. You.
3155: \newblock Unfolding partiality and disjunctions in stable model semantics.
3156: \newblock In A.G. Cohn, F.~Giunchiglia, and Selman B., editors, {\em Principles
3157: of Knowledge Representation and Reasoning: Proceedings of the 7th
3158: International Conference}, Breckenridge, Colorado, April 2000. Morgan
3159: Kaufmann.
3160:
3161: \bibitem{KLP03:aij}
3162: C.~Koch, N.~Leone, and G.~Pfeifer.
3163: \newblock Enhancing disjunctive logic programming systems by {SAT} checkers.
3164: \newblock {\em Artificial Intelligence}, 151:177--212, 2003.
3165:
3166: \bibitem{Kripke75:jp}
3167: S.~Kripke.
3168: \newblock Outline of a theory of truth.
3169: \newblock {\em Journal of Philosophy}, 72:690--716, 1975.
3170: \newblock Reprinted in: R. Martin, ed., {\em Recent Essays on Truth and the
3171: Liar Paradox} (Clarendon Press, Oxford, 1984) 53-81.
3172:
3173: \bibitem{DLV}
3174: N.~Leone et~al.
3175: \newblock A disjunctive datalog system \sys{dlv} (2003-05-16).
3176: \newblock Available under \url{http://www.dbai.tuwien.ac.at/proj/dlv/},
3177: 2003.
3178:
3179: \bibitem{LPFEGPS03:submitted}
3180: N.~Leone, G.~Pfeifer, W.~Faber, T.~Eiter, G.~Gottlob, and F.~Scarcello.
3181: \newblock The \sys{dlv} system for knowledge representation and reasoning.
3182: \newblock CoRR: cs.AI/0211004 v2, August 2003.
3183: \newblock Submitted for publication.
3184:
3185: \bibitem{LRS97:ic}
3186: N.~Leone, L.~Rullo, and F.~Scarcello.
3187: \newblock Disjunctive stable models: Unfounded sets, fixpoint semantics, and
3188: computation.
3189: \newblock {\em Information and Computation}, 135(2):69--112, 1997.
3190:
3191: \bibitem{Lifschitz99:iclp}
3192: V.~Lifschitz.
3193: \newblock Answer set planning.
3194: \newblock In {\em Proceedings of the 16th International Conference on Logic
3195: Programming}, pages 25--37, Las Cruces, New Mexico, December 1999. MIT Press.
3196:
3197: \bibitem{LY01:ijcai}
3198: F.~Lin and J.~You.
3199: \newblock Abduction in logic programming: a new definition and an abductive
3200: procedure based on rewriting.
3201: \newblock In {\em Proceedings of the Seventeenth International Joint Conference
3202: on Artificial Intelligence}, pages 655--661, Seattle, Washington, U.S.A.,
3203: August 2001.
3204:
3205: \bibitem{LZ02:aaai}
3206: F.~Lin and Y.~Zhao.
3207: \newblock \sys{assat}:
3208: Computing answer sets of a logic program by {SAT} solvers.
3209: \newblock In {\em Proceedings of the Eighteenth National Conference on
3210: Artificial Intelligence}, pages 112--117, Edmonton, Alberta, Canada,
3211: July--August 2002. AAAI.
3212:
3213: \bibitem{LRS98:tacas}
3214: X.~Liu, R.~Ramakrishnan, and S.~Smolka.
3215: \newblock Fully local and efficient evaluation of alternating fixed points.
3216: \newblock In Bernhard Steffen, editor, {\em Proceedings of the 4th
3217: International Conference on Tools and Algorithms for the Construction and
3218: Analysis of Systems}, pages 5--19, Lisbon, Portugal, March/April 1998.
3219: Springer-Verlag.
3220:
3221: \bibitem{MT91:jacm}
3222: W.~Marek and M.~Truszczy\'{n}ski.
3223: \newblock Autoepistemic logic.
3224: \newblock {\em Journal of the ACM}, 38:588--619, 1991.
3225:
3226: \bibitem{MT99:lpp}
3227: W.~Marek and M.~Truszczy\'{n}ski.
3228: \newblock Stable models and an alternative logic programming paradigm.
3229: \newblock In {\em The Logic Programming Paradigm: a 25-Year Perspective}, pages
3230: 375--398. Springer-Verlag, 1999.
3231:
3232: \bibitem{Niemela96:tab}
3233: I.~Niemelä.
3234: \newblock A tableau calculus for minimal model reasoning.
3235: \newblock In {\em Proceedings of the Fifth Workshop on Theorem Proving with
3236: Analytic Tableaux and Related Methods}, pages 278--294, Terrasini, Italy, May
3237: 1996. Springer-Verlag.
3238:
3239: \bibitem{Niemela99:amai}
3240: I.~Niemelä.
3241: \newblock Logic programming with stable model semantics as a constraint
3242: programming paradigm.
3243: \newblock {\em Annals of Mathematics and Artificial Intelligence},
3244: 25(3,4):241--273, 1999.
3245:
3246: \bibitem{Przymusinski90:iclp}
3247: T.~Przymusinski.
3248: \newblock Extended stable semantics for normal and disjunctive logic programs.
3249: \newblock In {\em Proceedings of the 7th International Conference on Logic
3250: Programming}, pages 459--477. MIT Press, 1990.
3251:
3252: \bibitem{Przymusinski90:fi}
3253: T.~Przymusinski.
3254: \newblock Well-founded semantics coincides with three-valued stable semantics.
3255: \newblock {\em Fundamenta Informaticae}, 13:445--463, 1990.
3256:
3257: \bibitem{RM95:nmelp}
3258: C.~Ruiz and J.~Minker.
3259: \newblock Computing stable and partial stable models of extended disjunctive
3260: logic programs.
3261: \newblock In {\em Nonmonotonic Extensions of Logic Programming}, pages
3262: 205--229. Springer, 1995.
3263: \newblock LNCS 927.
3264:
3265: \bibitem{Sacca97:jcss}
3266: D.~Sacc\`{a}.
3267: \newblock The expressive powers of stable models for bound and unbound datalog.
3268: \newblock {\em Journal of Computer Systems and Sciences}, 54(3):441--464, 1997.
3269:
3270: \bibitem{Sacca90:pods}
3271: D.~Sacc\`{a} and C.~Zaniolo.
3272: \newblock Stable models and non-determinism in logic programs with negation.
3273: \newblock In {\em Proceedings of the 9th ACM Symposium on Principles of
3274: Database Systems}, pages 205--217, 1990.
3275:
3276: \bibitem{SSW96:jicslp}
3277: K.~Sagonas, T.~Swift, and D.~Warren.
3278: \newblock An abstract machine for computing the well-founded semantics.
3279: \newblock In M.~Maher, editor, {\em Proceedings of the Joint International
3280: Conference and Symposium on Logic Programming}, pages 274--288, Bonn,
3281: Germany, September 1996. MIT Press.
3282:
3283: \bibitem{SS97:jlp}
3284: C.~Sakama and H.~Seki.
3285: \newblock Partial deduction in disjunctive logic programming.
3286: \newblock {\em Journal of Logic Programming}, 32(3):229--245, 1997.
3287:
3288: \bibitem{Schlipf95:jcss}
3289: J.~Schlipf.
3290: \newblock The expressive powers of the logic programming semantics.
3291: \newblock {\em Journal of Computer and System Sciences}, 51:64--86, 1995.
3292:
3293: \bibitem{SMR97:ilps}
3294: D.~Seipel, J.~Minker, and C.~Ruiz.
3295: \newblock A characterization of the partial stable models for disjunctive
3296: databases.
3297: \newblock In {\em International Logic Programming Symposium}, pages 245--259,
3298: 1997.
3299:
3300: \bibitem{GNT}
3301: P.~Simons and T.~Janhunen.
3302: \newblock \sys{GnT1} and \sys{GnT2} -- two solvers for disjunctive logic
3303: programs.
3304: \newblock Available in the World Wide Web under
3305: \url{http://www.tcs.hut.fi/Software/gnt/}, 2003.
3306:
3307: \bibitem{SNS02:aij}
3308: P.~Simons, I.~Niemelä, and T.~Soininen.
3309: \newblock Extending and implementing the stable model semantics.
3310: \newblock {\em Artificial Intelligence}, 138(1--2):181--234, 2002.
3311:
3312: \bibitem{SMODELS}
3313: P.~Simons and T.~Syrjänen.
3314: \newblock \sys{smodels} and \sys{lparse} -- a solver and a grounder for normal
3315: logic programs.
3316: \newblock Available in the World Wide Web under
3317: \url{http://www.tcs.hut.fi/Software/smodels/}, 2003.
3318:
3319: \bibitem{Stockmeyer77:tcs}
3320: L.~Stockmeyer.
3321: \newblock The polynomial-time hierarchy.
3322: \newblock {\em Theoretical Computer Science}, 3:1--22, 1977.
3323:
3324: \bibitem{SM73:stoc}
3325: L.~Stockmeyer and A.~Meyer.
3326: \newblock Word problems requiring exponential time.
3327: \newblock In {\em Proceedings of the 5th Annual ACM Symposium on the Theory of
3328: Computing}, pages 1--9, 1973.
3329:
3330: \bibitem{Syrjanen00:cl}
3331: T.~Syrjänen.
3332: \newblock Including diagnostic information in configuration models.
3333: \newblock In {\em Proceedings of the First International Conference on
3334: Computational Logic}, pages 837--851, London, U.K., July 2000.
3335: Springer-Verlag.
3336:
3337: \bibitem{YY94:jcss}
3338: J.~You and L.~Yuan.
3339: \newblock A three-valued semantics for deductive databases and logic programs.
3340: \newblock {\em Journal of Computer Systems and Sciences}, 49:334--361, 1994.
3341:
3342: \end{thebibliography}
3343:
3344:
3345: \end{document}
3346:
3347:
3348:
3349: