The use of recursive aggregates in Answer Set Programming (ASP) was so far limited because current solvers only deal with monotone aggregates. The grounder is thus in charge for rewriting aggregates into the more constrained form accepted by solvers. However, until now, no rewriting that correctly transform non-convex aggregates was known. This is going to change soon! Give a try to this script on my GitHub. File
README, reported below, should give enough information on how to use the script.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33
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 Solving... 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) SATISFIABLE 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.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38
$ ./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.