Wissensverarbeitung und Informationssysteme

[Photo]

noMoRe
A Graph-Based System for Non-Monotonic Reasoning with Logic Programs under Answer Set Semantics

Thomas Linke

Andreas Bösel

Christian Anger

Universität Potsdam, Institut für Informatik


Contents


Download

The former pre-releases of noMoRe [] are still available:1. former noMoRe release.


Introduction

noMoRe is an answer set solver for propositional normal nested logic programs. Those programs are sets of rules of the following form:
\begin{displaymath}
h_1,\ldots ,h_k \leftarrow B_1;\ldots ; B_n
\end{displaymath} (1)

where $h_1,\ldots ,h_k$ are propositional atoms and $B_1,\ldots ,B_n$ are conjunctions of literals or $\top$ (true) or $\bot$ (false). Here by a literal we mean either a propositional atom $a$ or the default negation of some propositional atom $\ensuremath{not}\; a$. For a rule $r$ of the form (1) $\ensuremath{\mathit{head}(r)}$ and $\ensuremath{\mathit{body}(r)}$ denote the sets $\{h_1,\ldots ,h_k\}$ and $\{B_1,\ldots ,B_n\}$, respectively. noMoRe implements a novel graph-based paradigm to compute answer sets by computing non-standard graph colorings of the rule dependency graph (RDG) of a given logic program $P$. The RDG of normal nested logic programs is a generalization of the RDG graph of normal programs as defined in [5,4].2It contains information about the positive (arcs in $\ensuremath{A^0_{}}$) and negative (arcs in $\ensuremath{A^1_{}}$) dependencies between rules: The RDG of a program $P$ is denoted by $\ensuremath{\Gamma_{P}}$.
\begin{definition}
Let $P$ be a normal nested logic program.
The \emph{rule dep...
...\ensuremath{\mathit{body}(\r)}
\}.
\end{array}\end{displaymath}\end{definition}
Intuitively, an a-coloring of $\ensuremath{\Gamma_{P}}$ is a non-standard 2-coloring reflecting application and non-application of the rules in $P$. In fact, the a-colorings of $\ensuremath{\Gamma_{P}}$ correspond to the answer sets of $P$. The generating rules of an answer set are colored with the first color reflecting application. Rules in the complement of the generating rules (wrt $P$) are colored with the second color reflecting non-application.

Given a logic program noMoRe first computes the corresponding rule dependency graph. Next the a-colorings of the RDG are computed. These are finally reinterpreted as answer sets of the underlying logic program. The core system was designed for propositional programs only. Thus, we have integrated different grounders (lparse and dlv ) in order to deal with variables. Because neither lparse nor dlv can hanlde normal nested programs, only normal programs can be processed, when variables are present.

The graph-based approach of the noMoRe system allows for a structural analysis of programs. Therefore, noMoRe comes with some a-coloring preserving graph transformations for RGDs which are able to speed up the coloring procedure. The basic idea of those transformations is to contract a set of nodes to a single node whenever all nodes of the set have the same color for each a-coloring. See [6] for details on graph transformations and normal nested programs.

Furthermore, we have included an interface to the graph drawing tool daVinci [7] for visualization of RDGs and their colorings [3]. The noMoRe-system is implemented in ECLiPSe Prolog3and is available at http://www.cs.uni-potsdam.de/wv/nomore.


Installation

In order to install noMoRe, you need to have a correctly installed ECLiPSe system on your machine. To use all features of the system, including the visual output of graphs, a correctly installed daVinci  [7] is also required. If you want to use normal logic programs with variables you also need to have installed lparse 4. Installation under Unix/Linux then is very easy; you just need to unpack the file nomore.tar.gz. In order to install noMoRe type the following:
> gunzip nomore.tar.gz
> tar -xvf nomore.tar
This results in a new directory named noMoRe containing all necessary files (see Section 8).

If you detect any bugs or errors please send an e-mail to the noMoRe developer group.


Getting Started

The best way of getting started is to consult an exemplary session under ECLiPSe Prolog [1]. We start this session in the subdirectory noMoRe/Examples by invoking ECLiPSe . This has the advantage that we have direct access to the *.lp files which contain different exemplary logic programs. We proceed in the following way:
  1. Start ECLiPSe .
  2. Next load noMoRe by typing [nomore]. <Ret> to the prolog-prompt.
    [eclipse 1]: [nomore].
    
    ...
    
    ----------- User Flags --------------
    capture        = on
    transform      = on
    backprop       = on
    ignore         = on
    show           = off
    animate        = off
    names          = off
    internal       = off
    ground         = off
    
    nomore.pl  compiled traceable 28 bytes in 0.06 seconds
    
    Yes (0.06s cpu)
    [eclipse 2]:
    
    This consults all necessary files and the actual flag settings (stored in file flags.ini) of the noMoRe system are printed on the screen. In order to get a printout of the current flag settings you may also type flags. to the prolog prompt any time after consluting the noMoRe source code. See Section 6 for details on how to change system behavior by setting or clearing binary noMoRe-flags.
  3. Let us consider a small example program stored in file penguin.lp containing the following logic program:
    \begin{displaymath}
P = \left\{ \!
\begin{array}{lclcl}
r_1 &\;:\;\;& bird & \le...
...\
r_5 &\;:\;\;& wings & \leftarrow & bird
\end{array}\right\}
\end{displaymath} (2)

    With the command nomore/2 (see Section 6) the desired number of answer sets for the program of the given file are computed. noMoRe also gives information about the time used and about how many solutions were found and how many choices and assignments were needed in order to compute the answer sets of a given logic program.
    [eclipse 3]: nomore('penguin.lp',0).
    
    noMoRe now computes all answer sets (indicated through the zero as second argument of nomore/2) of logic program (2).
    parsing file ../Examples/penguin.lp ...
    5 rules and 0 preference successfully parsed
    parsing done
    
    program transformation ... done
    
    computing rule dependency graph ... done
    
    computing answer sets ...
    
    Answer Set 1: { bird, fly, penguin, wings }
    
    Answer Set 2: { bird, nofly, penguin, wings }
    
    answer sets done
    
    ---------------------------------------------
    total number of assignments   : 19
    total number of choices       : 1
    ---------------------------------------------
    
    number of solutions        : 2  (for program ../Examples/penguin.lp)
    duration                   : 0.0s
    
    [eclipse 4]:
    
    After compiling the rule dependency graph of the program located in file penguin.lp, all a-colorings are computed. In this case, we have two different a-colorings for the penguin example (2) which correspond to the two answer sets (see Figure 7). It is also possible to give the number of answer sets to be computed, by giving a number $k>0$ as the second argument to the command nomore/2. For example, to compute only one answer set type nomore('penguin.lp',1).

  4. For getting a visual of the RDG simply type set_flag(show) which sets the noMoRe-flag show. Repeat the last command: nomore('penguin.lp',1). Now noMoRe starts the graph drawing tool daVinci and sends the actual RDG to daVinci before the answer sets of penguin.lp are computed. Different kinds of animated coloring sequences are possible, depending on the current settings. See Section 7 for information on how to control the animated coloring sequences depicted in daVinci .
Other example files can be processed analogously.


Architecture

noMoRe computes answer sets of a normal nested logic program in two steps (see  Figure 1)5.
Figure 1: The architecture of noMoRe.
\begin{figure}\begin{center}
\psset{arrows=->,fillcolor=white,fillstyle=solid}
...
...i}
\ncline{D}{F}
\end{pspicture} \end{center}\par
\vspace{-5ex}
\end{figure}
At first, the RDG is computed and possibly simplified according to the setting of flag transform. Secondly, the a-colorings of the RDG are computed by an efficient coloring procedure. To read logic programs we use a parser and there is a separate part for interpretation of a-colorings into answer sets. For information and debugging purposes there is yet another part for visualizing RDGs using the graph drawing tool daVinci  [7]. This feature is especially interesting for analyzing small programs (around 50 rules). Even if the core system was designed for propositional logic programs, it is possible to handle normal logic programs with variables. By setting the ground flag lparse [9] is used for grounding, and a file <name>.glp is created which contains the ground program corresponding to program <name>.lp6.

For example, by setting the flag names the RDG of program (2) is depicted as in Figure 2, that is, the actual rules are used as node labels. On the other hand, if the flag names is cleared then the internal noMoRe symbols are used as node labels. Depending on the size of the program under consideration both settings are useful.

Figure 2: The rule dependency graph of program (2). With flag names set (left) and cleared (right).
\scalebox{0.6}{\includegraphics{penguin.ps}} \scalebox{0.6}{\includegraphics{penguin1.ps}}


Syntax

In general, noMoRe deals with propositional normal nested logic programs. The syntax accepted by the system is Prolog-like, except that noMoRe accepts each ground Prolog term as a propositional atom, e.g. $p(a)$ and $q(a,b)$ are both treated as propositional atoms. As indicated in the formal definition (1), conjunction is allowed in the body and in the head, whereas disjunction is only allowed in the body in order to form disjunctions of conjunctions as bodies. Each line beginning with a % is regarded as a comment line. For example, normal logic program (2) is represented by the following file:
       penguin.
       bird :- penguin.
       wings :- bird.
       fly :- bird, not nofly.
       nofly :- penguin, not fly.
For another example, we consider the rule $\ensuremath{a,b \leftarrow (c,\ensuremath{not}\;d);(e)}$ with nested body. Rules like this can be expressed as
       a,b :- (c, not d);(e).
in noMoRe.

It is also possible to include so called integrity constraints as rules into a logic program. Integrity constraints have the form

       :- p1, ... ,pn.
Intuitively, an integrity constraint states that there should be no answer set which contains all of the atoms p1, ... ,pn.

Furthermore, we have cardinality constraints and weight constraints as described in [8] A cardinality constraint has the form

  Low {p1, ..., pn} Up
where Low and Up are integers representing the lower and upper bound for the number of atoms from p1, ... ,pn which must be true. For example,
  d :- 1 {a,b,c} 2.
can be read as ``$d$ is true if at least one and at most two of the literals $a,b,c$ are true''. That is $d$ is satisfied if any one atom of the set $\{a,b,c\}$ is true or any combination of two atoms from $\{a,b,c\}$ is true, but not if all three of them are true. Either of the bounds can be omitted, in which case they are to be taken as $-\infty$ and $\infty$[8].

Weight constraints are a generalization of cardinality constraints. One can assign a certain weight to each literal and the lower and upper bound represent weights also. A weight constraint is of the form

  Low [p1=w1, p2=w2, ..., pn=wn] Up
where Low and Up are integers and again represent the lower and upper bound. Every literal $p_{i}, 1 \leq i \leq n$ has been assigned a certain weight $\omega_{i}, 1 \leq i \leq n$. For example,
  d :- 2 [a=1, b=2, c=3] 3.
can be read as ``$d$ is true, if the sum of the weights of the true literals is at least 2 and at most 3'' That is, $d$ is true only if either just $b$ or $a$ and $b$ are true, or $c$ is true, but not if all three are true. For more information on weight and cardinality constraints see [2].


Commands and Configuration

Working with logic programs:

There are the following commands for computing answer sets of propositional logic programs stored in file <File>.

Accessing flag values:

Each flag <Flag> is represented by some ground Prolog term. With the commands set_flag/1 and clear_flag/1 it is possible to set and clear the available binary flags of the noMoRe system. For a listing of all flags and their current settings use command flags/0. Default flag settings are defined in file noMoRe/Source/flags.ini. You can change the behavior of noMoRe by editing this file or using the following commands during a prolog session to change the flag settings. A description of all currently supported flags is shown in Table 1. By just giving a valid flag name from that Table as a command to noMoRe the corresponding flag is toggled, that is, the flag is cleared if it is currently set and vis versa. This provides the user with some nice shortcuts to influence the system behavior.

Observe, that some flags depend on some other flags. More precisely, flag animate depends on flag show, because the dynamic visualization of the construction of some a-coloring of the RDG is only possible if the graph was visualized before. noMoRe automatically keeps track of flag dependencies, this means, if the user sets flag animate then flag show will be automatically set if it is currently cleared and vis versa. If both flags animate and show are set and the user clears flag show then flag animate is cleared automatically.

Table 1: Supported noMoRe-flags
flag controls default
capture transformation of a given program to a captured one on
transform graph transformations on
backprop backward propagation on
ignore if a rule with a certain head is colored with $\oplus$, then all other rules with same head are ignored on
show visualization of the RDG off
animate dynamic visualization of coloring off
names node labels; instead of internal noMoRe symbols the actual rules are used as node labels of the RDG off
internal toggles between the actual RDG and the noMoRe internal representation of the RDG as body-rule-head graph off
ground use of lparse as grounder; if set, the ground version of a program located in a file named <name>.lp is written into a file named <name>.glp. off


Miscellaneous commands:


Visualization

The flags show, animation and names influence the visualization component of the noMoRe system. By setting flag show the visualization is activated, which enables noMoRe to use daVinci as output tool for rule dependency graphs and their colorings. After calling the command nomore/2 (or nomore/4) the daVinci API is used to draw the actual RDG. The flag names determines if the original rules of a program (names set) or the internal noMoRe identifiers (names cleared) are used as node labels. By setting the flag animation the daVinci API is used to animate the noMoRe coloring procedure during run time. So noMoRe is not a black box anymore but a vitreous one. Furthermore, the animated coloring sequences may be used for debugging of small logic programs under answer set semantics, because the user gets access to the full construction process of the answer sets. Hence we are able to detect the rules which are responsible for a specific answer sets.

Let's demonstrate the visualization component by computing the answer sets of program (2):

  1. Start ECLiPSe , load noMoRe and ensure that flag show is set by set_flag(show). This activates the visualization tool. Furthermore, ensure that the flag animation is set by set_flag(animation), since we are interested in an animated coloring sequence. Observe, that due to flag dependency handling it is sufficient to set flag animation; then flag show is set automatically.
  2. Continue by typing nomore('penguin.lp',0). After noMoRe has computed the RDG of program (2) it is translated in the daVinci term representation. Then daVinci is started as a child process and the translated RDG is send to daVinci . Figure 7 illustrates the output after an initial coloring step.
  3. Now daVinci takes control and awaits an input by the user in order to process a number of coloring steps (a coloring step is the coloring of exactly one node.). The number of coloring steps which are preformed without interruption depends on the setting of the Edit submenu Stopping criterion of daVinci . By default it is set to every node, which causes the noMoRe coloring procedure to stop after each single coloring step. However, now we are able to change some daVinci specific settings, such as Node presentation, Stopping criterion and Animation speed. For a complete description of the posssible daVinci settings see Table 2. Finally, to continue the computation type Alt-G or click the Go-icon on the upper left side of the daVinci window.
  4. Step by step every coloring of the noMoRe algorithm is visualized in daVinci . Observe that nodes which are used as choices during computation are marked by a double circle.
  5. Finally an a-coloring is obtained (Figure 7). The corresponding answer set is {bird, nofly, penguin, wings}. The noMoRe algorithm tries to compute other a-colorings via backtracking. This is modeled by discoloring the corresponding nodes. See Figure 7 for the complete coloring sequence for program (2).

Figure 3: The rule dependency graph of (2) after the first coloring step.
\scalebox{0.5}{\includegraphics{penguin2.ps}}

Figure 4: The rule dependency graph of (2) after a second coloring step.
\scalebox{0.5}{\includegraphics{penguin3.ps}}

Figure 5: A complete coloring.
\scalebox{0.5}{\includegraphics{penguin6.ps}}

Figure 6: The complete coloring sequence for program (2).
\scalebox{0.4}{\includegraphics{penguin1.ps}} \scalebox{0.4}{\includegraphics{penguin2.ps}} \scalebox{0.4}{\includegraphics{penguin3.ps}} \scalebox{0.4}{\includegraphics{penguin4.ps}}
\scalebox{0.4}{\includegraphics{penguin5.ps}} \scalebox{0.4}{\includegraphics{penguin6.ps}} \scalebox{0.4}{\includegraphics{penguin7.ps}} \scalebox{0.4}{\includegraphics{penguin7.1.ps}}
\scalebox{0.4}{\includegraphics{penguin8.ps}} \scalebox{0.4}{\includegraphics{penguin9.ps}} \scalebox{0.4}{\includegraphics{penguin8.ps}} \scalebox{0.4}{\includegraphics{penguin7.1.ps}}

Beside the flags show, animation and names (see Table 1) there are several settings that affect the style of the visualization. Those settings are accessible via the Edit menu of daVinci . See Table 2 for a complete listing of all possibilities to influence the presentation of RDGs and their animated colorings. By right clicking on a single node it is also possible to change the node representation of that node.

Please observe: If the flag transform is set, noMoRe applies some graph transformations. Sets of nodes are transformed to one single node if they will have the same color for all a-colorings. Hence nodes are no longer representing single rules but set of rules. Therefore the nodes of the visualized graph are only labeled by noMoRe internal identifiers and the node presentation cannot be changed in this case.

noMoRe internally represents the RDG as the so called body-rule-head (BRH-)graph. Each body, rule and head of a program correspond to some single node in the BRH graph. Then some node (rule) $N$ in the RDG corresponding to normal rule $\ensuremath{\ensuremath{\mathit{head}(N)} \leftarrow \ensuremath{\mathit{body}(N)}}$ in the underlying program is represented as a linear ordered subgraph $\ensuremath{\mathit{body}(N)}\rightarrow N\rightarrow\ensuremath{\mathit{head}(N)}$ in the BRH graph. If we take a general rule of the form (1) then in the above subgraph we would obtain several bodies as predecessors of $N$ and several heads as successors of $N$. The flag internal causes noMoRe to use the body-rule-head graph for visualization. If one is interested in the internal data structure of noMoRe, which currently is the BRH graph, then the flag internal should be set.

Table 2: Possibilities to influence the representation of RDGs and their animated colorings via the Edit submenu of daVinci .
Edit menu items shortcut function
Toggle Node Labels Alt-T toggles between internal noMoRe identifiers and the actual rules as node labels (same as flag names)
Toggle Dependency Graph Alt-I toggles between the actual RDG and the noMoRe internal representation of the RDG as BRH graph (same as flag internal)
Go Alt-G start animation until stopping criterion is reached
Abort Alt-A abort answer set computation and exit daVinci
Stop At none submenu for choosing one of the following as stopping criterion for the animation: Choices, Each Node, Full Coloring, No Stop
Animation Speed none submenu for choosing the speed of animation, possible choices are: Slow, Normal, Fast



The Files

The noMoRe system comes in the following files and directories:
/nomore/Source
The source files of the system:
/nomore/Source/algorithm.pl

Contains the algorithmic code of the coloring problem including all propagation cases.

/nomore/Source/blockgraph.pl

The rule dependency graph (block graph) corresponding to a logic program $P$ is computed with procedures defined in this file.

/nomore/Source/call_count.pl

Some statistic informations are collected.

/nomore/Source/commands.pl

Contains the main noMoRe-commands.

/nomore/Source/daVinci.pl

Here the daVinci term representation of a RDG is computed.

/nomore/Source/eclipse.pl and /nomore/Source/swi.pl

These two files contain Prolog system specific code.

/nomore/Source/flags.pl

Contains predicates for accessing flags.

/nomore/Source/graphs.pl

Here, graph operations are provided.

/nomore/Source/heuristics.pl

Contains predicates for dynamic heuristics. Under development.

/nomore/Source/io.pl

This file contains the noMoRe predicates for reading (writing) logic programs from (into) files.

/nomore/Source/nomore.pl

Here all necessary files are consulted and the default flag settings are provided. One can influence the system behavior by activating or deactivating the binary flags by editing noMoRe. Please observe that setting the output-flag will slow down the time measurements tremendously, since the output procedure is not optimized.

/nomore/Source/parser.pl

This file contains the parser which reads a logic program out of a file and performs a syntax check. For grounding programs with variables lparse is used if the belonging flag is set.

/nomore/Source/reduction.pl

This file contains algorithms for reducing the number of nodes of the RDG. For more details and further descriptions see [6].

/nomore/Source/symbolize.pl

This file contains predicates which introduces names for the rules of the logic program.

/nomore/Doc

This documentation is located here.

/nomore/Examples

This directory contains some examples. For more details about the examples see file /noMoRe/Examples/README. It can also be used to store your own examples.
Observe, that each directory contains the file nomore.pl which consults the necessary source files from /nomore/Source. This way, one can consult noMoRe simply by typing [nomore]. to the prompt of a running Prolog system in each of the subdirectories.

The noMoRe system automatically generates the following files in the current working directory:

./<name>.daVinci

This is the generated file for daVinci if the correspondig flag is set.

It is written if the daVinci flag is set and contains the RDG in a format readable by the graph drawing tool daVinci . <name> or <name>.lp corresponds to the input file's name.

./<name>.glp

is written if the lparse flag is set and contains the ground logic program corresponding to <name> or <name>.lp.

Bibliography

1
A. Aggoun, D. Chan, P. Dufresne, et al.
Eclipse user manual release 5.0, 2000.

2
C. Anger.
Constraint transformation.
http://www.cs.uni-potsdam.de/~christian/translation/, 2001.

3
A. Bösel, T. Linke, and T. Schaub.
Profiling answer set programming: The visualization component of the noMoRe system.
2003.
submitted to LPNMR.

4
K. Konczak, T. Linke, and T. Schaub.
Graphs and colorings for answer set programming: Abridged report.
2003.
Submitted to LPNMR.

5
T. Linke.
Graph theoretical characterization and computation of answer sets.
In B. Nebel, editor, Proceedings of the International Joint Conference on Artificial Intelligence, pages 641-645. Morgan Kaufmann Publishers, 2001.

6
T. Linke.
Using nested logic programs for answer set programming.
2003.
submitted to LPNMR.

7
M.Werner.
davinci v2.1.x online documentation, 1998.

8
I. Niemelä and P. Simons.
Extending the smodels system with cardinality and weight constraints.
Logic-Based Artificial Intelligence, pages 491-521, 2000.

9
T. Syrjänen.
Lparse 1.0 user's manual, 2000.