Full aggregate support

[madmike200590]

Full Aggregate Support

This PR adds support for

• Arbitrary comparison operators for aggregate literals, notably enables aggregate literals binding variables through equality, e.g. X = #count{N : thing(N)}.
• Aggregate functions min and max
• Lower- and Upper-Bound operators and terms, e.g. X < #sum{...} < Y
• Arbitrary number of aggregate literals per rule

Implementation

As before, aggregates are supported by rewriting aggregate literals to aggregate-free sub-programs. The basic workflow for this is implemented in AggregateRewriting:

• First, split up aggregate literals with two operators into two separate literals.
• Afterwards, normalize operators: For count and sum, all aggregate literals are rewritten into versions that only use = and <= as operators.
• After these preparation steps, substitute aggregate literals in rule body with generated standard literals representing the aggregate and add the respective sub-programs.

Aggregate Literal Splitting

This process step transforms aggregate literals that have both a lower- and upper-bound operator into two literals with only lower-bound operators while preserving semantics.
For positive literals, this is straight-forward - the lower-bound operator stays unchanged, and a second instance of the literal is added to the rule where the former upper-bound term is used as lower-bound term and the operator "turned" accordingly, e.g.

count_between(X, Y) :- dom(X), dom(Y), X < #count(I : cnt_dom(I)) < Y.

is transformed into

count_between(X, Y) :- dom(X), dom(Y), X < #count{I : cnt_dom(I)}, Y > #count{I : cnt_dom(I)}.

Slightly more effort is needed for negated aggregate literals. Since the semantics of the literal not X <op1> <aggr> <op2> Y is NOT (X <op1> <aggr> AND <aggr> <op2> Y), and therefore after applying DeMorgan's rule: NOT (X <op1> <aggr>) OR NOT (<aggr> <op2> Y), this cannot be directly represented in one rule (since ASP does not support disjunction within rule bodies). Rules containing negated aggregate literals with two operators therefore need to be split into separate rules, e.g:

count_not_between(X, Y) :- dom(X), dom(Y), not X < #count(I : cnt_dom(I)) < Y.

is transformed into

count_not_between(X, Y) :- dom(X), dom(Y), not X < #count{I : cnt_dom(I)}.
count_not_between(X, Y) :- dom(X), dom(Y), not Y > #count{I : cnt_dom(I)}.

For rules with more than one aggregate literal, the splitting process happens recursively until there are no rules with un-split literals left.

Aggregate Operator Normalization

In order to keep the actual rewriting logic for the respective aggregate functions simple, aggregate literals that use the count or sum function are transformed such that only = and <= are used for comparisons. The transformation works according to the following equivalencies:

• X < #aggr{...} <==> XP <= #aggr{...}, XP = X + 1
• X != #aggr{...} <==> not X = #aggr{...}
• X > #aggr{...} <==> not X <= #aggr{...}
• X >= #aggr{...} <==> not XP <= #aggr{...}, XP = X + 1
• not X < #aggr{...} <==> not XP <= #aggr{...}, XP = X + 1
• not X != #aggr{...} <==> X = #aggr{...}
• not X > #aggr{...} <==> X <= #aggr{...}
• not X >= #aggr{...} <==> XP <= #aggr{...}, XP = X + 1

For details on the semantics involved, see the ASP Core2 Standard.

Aggregate Encoding

After aggregate literals are split and their operators normalized, the final step is to substitute the aggregate literals in rule bodies with generated standard literals and add the appropriate sub-programs that define rules deriving said literals. This process is implemented in AggregateRewriting.

#count/#sum

The encodings for both count and sum aggregates work on the same basic principle:

• Literals of form X <= #aggr{...} are encoded by way of counting (or adding up) starting from zero and checking if the resulting intermediate results exceed the value of X thereby making X a lower bound for #aggr{...}.
• Literals of form X = #aggr{...} that assign a value to a variable make use of the variant for the "<= scenario". Every potential count (or sum) that is a lower bound on the actual value is calculated and the greatest resulting lower bound is returned as the actual count/sum.

Example

The program

thing(1).
thing(2).
thing(3).

cnt_things(N) :- N = #count{ X : thing(X)}.

is rewritten to

thing(1).
thing(2).
thing(3).

% Rewritten source rule
cnt_things(N) :- count_1_result(count_1_no_args, N).

%%% Aggregate Encoding

% An element tuple represents an element that is being aggregated.
count_1_element_tuple(count_1_no_args, tuple(X)) :- thing(X).
% Map every element tuple to an integer (starting with 1)
count_1_input_number(ARGS, IDX) :- count_1_element_tuple(ARGS, TPL), _Enumeration(ARGS, TPL, IDX).

% Based on input numbers from above, calculate all (partial) sums
count_1_bound(count_1_no_args, 0).
count_1_sum(ARGS, 0, 0) :- count_1_bound(ARGS, _0).
count_1_span(ARGS, _Interval0) :- I1 = I - 1, count_1_input_number(ARGS, I), _interval(1..I1, _Interval0).
count_1_sum(ARGS, 0, 0) :- count_1_input_number(ARGS, _1).
count_1_sum(ARGS, I, S) :- count_1_sum(ARGS, I1, S), I1 = I - 1, count_1_span(ARGS, I).
count_1_sum(ARGS, I, S1) :- count_1_sum(ARGS, I1, S), S1 = S + 1, I1 = I - 1, count_1_input_number(ARGS, I).

% Find the greatest partial sum (which is the actual count)
count_1_sum_less_than(ARGS, LESS, THAN) :- count_1_sum(ARGS, _2, LESS), count_1_sum(ARGS, _3, THAN), LESS < THAN.
count_1_sum_has_greater(ARGS, NUM) :- count_1_sum_less_than(ARGS, NUM, _4).
count_1_result(ARGS, CNT) :- count_1_sum(ARGS, _5, CNT), not count_1_sum_has_greater(ARGS, CNT).

#min/#max

Encodings for min and max aggregates are very similar. Both define a "less_than" relation over the respective element tuples and designate the element that has no smaller (min) or greater (max) element as result.

Example

The program

thing(1).
thing(3).
thing(666).
thing(5).

max_thing(M) :- M = #max{ X : thing(X) }.

is rewritten to

thing(1).
thing(3).
thing(666).
thing(5).

% Rewritten source rule
max_thing(M) :- max_1_result(max_1_no_args, M).

%%% Aggregate Encoding

% Tuples to aggregate over
max_1_element_tuple(max_1_no_args, X) :- thing(X).

% Tuple ordering
max_1_element_tuple_less_than(ARGS, LESS, THAN) :- max_1_element_tuple(ARGS, LESS), max_1_element_tuple(ARGS, THAN), LESS < THAN.

% Find max tuple
max_1_element_tuple_has_greater(ARGS, TPL) :- max_1_element_tuple_less_than(ARGS, TPL, _0).
max_1_max_element_tuple(ARGS, MAX) :- max_1_element_tuple(ARGS, MAX), not max_1_element_tuple_has_greater(ARGS, MAX).
max_1_result(ARGS, M) :- max_1_max_element_tuple(ARGS, M).

[codecov]

Codecov Report

Merging #268 (3bfd498) into master (758e603) will increase coverage by 0.42%.
The diff coverage is 87.50%.

❗ Current head 3bfd498 differs from pull request most recent head 7777734. Consider uploading reports for the commit 7777734 to get more accurate results

@@             Coverage Diff              @@
##             master     #268      +/-   ##
============================================
+ Coverage     77.69%   78.12%   +0.42%     
- Complexity     2362     2465     +103     
============================================
  Files           179      187       +8     
  Lines          7896     8127     +231     
  Branches       1383     1418      +35     
============================================
+ Hits           6135     6349     +214     
- Misses         1333     1344      +11     
- Partials        428      434       +6     

Impacted Files	Coverage Δ
.../at/ac/tuwien/kr/alpha/common/atoms/BasicAtom.java	83.67% <0.00%> (-5.46%)	⬇️
...a/at/ac/tuwien/kr/alpha/common/rule/BasicRule.java	33.33% <0.00%> (-66.67%)	⬇️
...wien/kr/alpha/grounder/IndexedInstanceStorage.java	76.62% <ø> (ø)
.../at/ac/tuwien/kr/alpha/grounder/NaiveGrounder.java	85.42% <ø> (ø)
...ounder/transformation/VariableEqualityRemoval.java	87.69% <62.50%> (-9.14%)	⬇️
...grounder/transformation/PredicateInternalizer.java	74.19% <63.63%> (-9.14%)	⬇️
...der/transformation/IntervalTermToIntervalAtom.java	92.85% <72.72%> (-5.48%)	⬇️
...c/tuwien/kr/alpha/common/terms/ArithmeticTerm.java	67.77% <75.00%> (-2.23%)	⬇️
.../aggregates/encoders/AbstractAggregateEncoder.java	78.78% <78.78%> (ø)
...ac/tuwien/kr/alpha/common/atoms/AggregateAtom.java	56.86% <80.00%> (+6.86%)	⬆️
... and 33 more

---

Continue to review full report at Codecov.

Legend - Click here to learn more
Δ = absolute <relative> (impact), ø = not affected, ? = missing data
Powered by Codecov. Last update b081a01...7777734. Read the comment docs.

[madmike200590]

This is a big step forward. My comments are mostly stylistic suggestions, with the exception of the one that is a potential bug (as we discussed already).

Thanks for the feedback! All taken care of, except for very few cases where I think my initial solution was better than the suggested change (see respective comments). Please take another look!

[AntoniusW]

@madmike200590 what is the current status here? I see some conflicts due to recent changes in master and we had the discussion about negative weights, which in principle can be accommodated but incur a quite hefty performance drawback. My suggestion, for the time being, is to add a commandline flag for whether aggregates should be rewritten such that negative weights are allowed or not. Default should be no negative weights in aggregates and throwing an exception once they are encountered, where the exception hints at turning the commandline flag on if one really wants negative weights. What are your thoughts?

[madmike200590]

@madmike200590 what is the current status here? I see some conflicts due to recent changes in master and we had the discussion about negative weights, which in principle can be accommodated but incur a quite hefty performance drawback. My suggestion, for the time being, is to add a commandline flag for whether aggregates should be rewritten such that negative weights are allowed or not. Default should be no negative weights in aggregates and throwing an exception once they are encountered, where the exception hints at turning the commandline flag on if one really wants negative weights. What are your thoughts?

Conflicts are fixed, latest changes from master merged. On the negative integer question, as per our dicussion, I implemented the correct handling of negative values as the default behavior now. Cmdline-switch for lightweight version only supporting positive integers will be done by end of this week.

[madmike200590]

Conflicts are fixed, latest changes from master merged. On the negative integer question, as per our dicussion, I implemented the correct handling of negative values as the default behavior now. Cmdline-switch for lightweight version only supporting positive integers will be done by end of this week.

@AntoniusW This is now (finally!) finished. Support for negative integers in sum elements can be disabled using the -dni commandline switch. Please take another look and merge if everything looks good!