G-stable Models

Answer Set Programming (ASP) allow to represent and reason on incomplete knowledge under stable model semantics. G-stable models are a recent proposal for interpreting ASP programs with aggregates:

Michael Gelfond, and Yuanlin Zhang.
Vicious Circle Principle and Logic Programs with Aggregates.
Theory and Practice of Logic Programming, 14(4-5): 587-601 (2014).

G-stable models can be computed by means of the following python script: [GitHub].

File README, reported below, should give enough information on how to use the script.

The following tools are required:

- python 3: https://www.python.org/downloads/

- gringo 3: http://sourceforge.net/projects/potassco/files/gringo/3.0.5/

- clasp 3: http://sourceforge.net/projects/potassco/files/clasp/3.1.1/

- wasp 2: https://github.com/alviano/wasp/

To compute all G-stable models of program example1.asp, use the following command-line:

$ ./gelfondize.py example1.asp | clasp 0

If everything is OK, you should see the following output:

clasp version 3.1.1
Reading from stdin
Answer: 1
p(1) p(2) p(4)
Answer: 2

Answer: 3
Answer: 4

Models       : 4     
Calls        : 1
Time         : 0.001s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s)
CPU Time     : 0.000s

To use wasp as the back-end ASP solver, run the following:

$ ./gelfondize.py example1.asp | wasp -n=0
WASP 2.0

{p(2), p(1), p(4)}

If command 'gringo' is not in the PATH, use the -g flag:

$ ./gelfondize.py -g /path/to/gringo example1.asp

Flags for gringo can also be specified (at the end of the command line).

Since this is just a proof-of-concept, aggregates must be encoded using predicates. Run the script with flag --help-syntax for more instruction.

$ ./gelfondize.py --help-syntax

The syntax is almost conformant to ASP Core 2.0, with the exception of aggregates.
Moreover, predicates starting with the prefix 'gz_' are reserved for internal use
and must not be used by the user. Remember also to not hide them!

Supported aggregates are COUNT, SUM, AVG, MIN, MAX, EVEN, and ODD. Aggregate sets are
declared by means of predicate gz_set/3, where:

- the first argument is the ID of an aggregate;

- the second argument is an integer;

- the third argument is an atom.

The second argument is optional, with default value 1.

A COUNT aggregate can be added in a rule body by using predicate gz_count/3, where:

- the first argument is the ID of an aggregate;

- the second argument is a comparator among ">=", ">", "<=", "<", "=", "!=";

- the third argument is an integer.

Aggregates SUM, AVG, MIN, and MAX are similar, and use predicates gz_sum/3, 
gz_avg/3, gz_min/3, and gz_max/3.

An EVEN aggregate can be added in a rule body by using predicate gz_even/1, where
the argument is the ID of an aggregate. Aggregate ODD is similar, and uses
predicate gz_odd/1.

Remember that COUNT, EVEN, and ODD are applied on true atoms in the aggregate set,
while SUM, AVG MIN, and MAX are applied on the multiset of integers associated with
true atoms in the aggregate set.

Variables can be used taking into account the previous description.