F-stable Models

Answer Set Programming (ASP) allow to represent and reason on incomplete knowledge under stable model semantics. Support for non-convex recursive aggregates can be achieved by means of the rewriting proposed in the following paper:

Mario Alviano, Wolfgang Faber, and Martin Gebser.
Rewriting recursive aggregates in answer set programming: back to monotonicity.
Theory and Practice of Logic Programming, to appear.
Online draft: [PDF]

Download link: [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/

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

$ ./f-aggregates.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
var(exists,x1,1) var(exists,x2,2) var(forall,y1,2) var(forall,y2,3) int(5) unequal true(forall,y2,3) true(forall,y1,2) true(exists,x1,1)

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

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

$ ./f-aggregates.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.

$ ./f-aggregates.py --help-syntax

The syntax is almost conformant to ASP Core 2.0, with the exception of aggregates.
Moreover, predicates starting with the prefix 'f_' 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, and MAX. Aggregate sets are
declared by means of predicate f_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 f_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 f_sum/3, f_avg/3,
f_min/3, and f_max/3.

Remember that COUNT is 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.