|
Wissensverarbeitung und Informationssysteme
|
noMoRe
A Graph-Based System for Non-Monotonic Reasoning with Logic
Programs under Answer Set Semantics
Download
- Here
you can
download the current version of the noMoRe system (file
nomore.tar.gz).
- Download lparse (needed for dealing with variables).
- Download daVinci (needed for visualization of ruel dependency graphs).
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:
 |
(1) |
where
are propositional atoms and
are
conjunctions of literals or
(true) or
(false).
Here by a literal we mean either a propositional atom
or the default negation of some propositional atom
.
For a rule
of the form (1)
and
denote the sets
and
, 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
.
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
) and negative (arcs in
)
dependencies between rules:
The RDG of a program
is denoted by
.
Intuitively, an a-coloring of
is a non-standard 2-coloring
reflecting application and non-application of the rules in
.
In fact, the a-colorings of
correspond to the answer sets of
.
The generating rules of an answer set are colored with the first
color reflecting application.
Rules in the complement of the generating rules (wrt
) 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:
- Start ECLiPSe .
- 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.
- Let us consider a small example program stored in file penguin.lp
containing the following logic program:
 |
(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
as the second argument to the command
nomore/2.
For example, to compute only one answer set type nomore('penguin.lp',1).
- 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.
 |
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).
|
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.
and
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
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 ``
is true if at
least one and at most two of the literals
are true''. That is
is satisfied if any one atom of the set
is true or any
combination of two atoms from
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
and
[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
has
been assigned a certain weight
. For example,
d :- 2 [a=1, b=2, c=3] 3.
can be read as ``
is
true, if the sum of the weights of the true literals is at least 2 and
at most 3'' That is,
is true only if either just
or
and
are true, or
is true, but not if all three are true.
For more information on weight and cardinality constraints see [2].
Commands and Configuration
There are the following commands for computing answer sets of propositional
logic programs stored in file <File>.
- nomore/2: nomore(<File>,<N>) computes
<N> answer sets of logic program stored in file
<File>.
For
all answer sets are computed.
- nomore/4: nomore(<Name>,<N>,<AS>,<CP>) computes
<N> answer sets <AS> of logic program stored in file
<Name> and returns the number of choice points <CP>.
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.
- flags/0: flags shows the current
flag setting.
- set_flag/1:
set_flag(<Flag>) sets the flag
<Flag>.
set_flag(<Flag>) also accepts a prolog list
of noMoRe flags for <Flag>, which then are all set.
- clear_flag/1:
clear_flag(<Flag>) clears the flag <Flag>. After applying
this flag get_flag(<Flag>) fails.
clear_flag(<Flag>) also accept a prolog list
of flags for <Flag>, which then are all cleared.
- get_flag/1:
get_flag(<Flag>) is true iff the flag <Flag> is set.
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 ,
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 |
|
- clear/0: clear deletes all temporary files
in the current working directory.
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):
- 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.
- 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.
- 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.
- 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.
- 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.
|
Figure 4:
The rule dependency graph of (2) after a second
coloring step.
|
Figure 5:
A complete coloring.
|
Figure 6:
The complete coloring sequence for program (2).
|
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)
in the RDG corresponding to normal rule
in the underlying program
is represented as a linear ordered subgraph
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
and several
heads as successors of
.
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
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.
- 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.