Unexpected grounding blow-up in aggregates

[AbdallahS]

Given the following program

{ a(1..2) }.
{ t }.

strange3(I) :- a(IM), I=1..IM, 0 = #sum { 3 : t, L=1, L<=I }.
strange4(I,J,K) :- a(IM), a(JM), a(KM), I=1..IM, J=1..JM, K=1..KM, I<=J, J<=K, K<=I, 0 = #sum { 4 : t, L=1, L <= I, L <= J, L <= K, L<= I }.
okay5(I) :- a(IM), I=1..IM, I<=10, 0 = #sum { 5 : t, L=0..I }.

range(1..2).
okay6(I) :- a(IM), range(I), I<= IM, I>=1, 0 = #sum { 6 : t, L=1, L=0..I }.
okay7(I) :- a(IM), IM<=10, I=1..IM, 0 = #sum { 7 : t, L=0..I }.

When I look at the rule for strange3, I expect the ground version to contain a number of rules that depend on I, but I don't expect the number of elements in the aggregate to depend on I. The rule for strange4 is the blown-up version of it: for fixed values I=1, J=1, K=1, I expect there to be a single rule with an aggregate over one element. Instead, the number of elements in the aggregate scales with the cross-product of the potential domain for I, J, K (even though the concrete domain is a singleton, since these variables are fixed to 1).

The output of gringo --text is

{a(1)}.
{a(2)}.
{t}.
okay7(1):-a(1),0>=#sum{7:t}.
okay7(1):-a(2),0>=#sum{7:t}.
okay7(2):-a(2),0>=#sum{7:t}.
range(1).
range(2).
okay6(1):-a(1),0>=#sum{6:t}.
okay6(1):-a(2),0>=#sum{6:t}.
okay6(2):-a(2),0>=#sum{6:t}.
okay5(1):-a(1),0>=#sum{5:t}.
okay5(1):-a(2),0>=#sum{5:t}.
okay5(2):-a(2),0>=#sum{5:t}.
strange4(1,1,1):-a(1),a(1),a(1),0>=#sum{4:t;4:t;4:t;4:t;4:t;4:t;4:t;4:t}.
strange4(1,1,1):-a(1),a(2),a(1),0>=#sum{4:t;4:t;4:t;4:t;4:t;4:t;4:t;4:t}.
strange4(1,1,1):-a(1),a(1),a(2),0>=#sum{4:t;4:t;4:t;4:t;4:t;4:t;4:t;4:t}.
strange4(1,1,1):-a(1),a(2),a(2),0>=#sum{4:t;4:t;4:t;4:t;4:t;4:t;4:t;4:t}.
strange4(1,1,1):-a(2),a(1),a(1),0>=#sum{4:t;4:t;4:t;4:t;4:t;4:t;4:t;4:t}.
strange4(1,1,1):-a(2),a(2),a(1),0>=#sum{4:t;4:t;4:t;4:t;4:t;4:t;4:t;4:t}.
strange4(1,1,1):-a(2),a(1),a(2),0>=#sum{4:t;4:t;4:t;4:t;4:t;4:t;4:t;4:t}.
strange4(1,1,1):-a(2),a(2),a(2),0>=#sum{4:t;4:t;4:t;4:t;4:t;4:t;4:t;4:t}.
strange4(2,2,2):-a(2),a(2),a(2),0>=#sum{4:t}.
strange3(1):-a(1),0>=#sum{3:t;3:t}.
strange3(1):-a(2),0>=#sum{3:t;3:t}.
strange3(2):-a(2),0>=#sum{3:t}.

Small variations in the writing of the rule body that don't change the semantics let us recover an efficient grounding (see the okay rules).

[rkaminsk]

This is indeed unfortunate. Now I should adjust gringo to not accumulate the elements twice. However, note that the aggregate is simplified before being passed to the solver. This is just not reflected in the text output.

Another issue is that the current aggregate implementation does not perform well, when we want to encode small checks in rule bodies. With the current implementation there is some redundant processing, I have been planning to ground stratified aggregates using some other implementation since a long time. I never came around to do it.

In your case (but not knowing the full context), I would try to avoid the aggregate altogether.

➜ gringo test.lp | lpconvert --text
{a(1)}.
{a(2)}.
{t}.
strange3(1) :- a(1), not t.
strange3(1) :- a(2), not t.
strange3(2) :- a(2), not t

[rkaminsk]

Closing for now. This will be addressed in future clingo versions.