Feature: symmetry breaking inside aggregates and with multiple inequalities

[MaxOstrowski]

:- #count{W : match(M1,W), match(M2,W), match(M3,W), M1 != M2, M1 != M3, M2 != M3} >= 2.
:- #count{M : match(M,W1), match(M,W2), match(M,W3), W1 != W2, W1 != W3, W2 != W3} >= 2.

currently does not do anything.

Could do:

three_men(W) :- match(_,W), { M: match(M,W) } >= 3.
:- #count{W : three_men(W) } >= 2.
...

[MaxOstrowski]

Now translates to

#false :- 2 <= #count { W: match(M1,W), match(M2,W), match(M3,W), M1 < M2, M2 < M3 }.
#false :- 2 <= #count { M: match(M,W1), match(M,W2), match(M,W3), W1 < W2, W2 < W3 }.

@rkaminsk Now your case gets detected, but it is not yet replaced with counting aggregates. I'm not yet sure if counting is always better than e.g. a quadratic rule. See #56. Maybe you have an opinion about it.

[rkaminsk]

Now your case gets detected, but it is not yet replaced with counting aggregates. I'm not yet sure if counting is always better than e.g. a quadratic rule. See #56. Maybe you have an opinion about it.

The rule above is not quadratic but cubic. So there is a real chance that the aggregate performs better. The problem is from https://www.mat.unical.it/aspcomp2013/OfficialProblemSuite. It is problem O15. You can download a tarball with instances here: https://www.mat.unical.it/ianni/aspcomp2013instances/b15.tar.gz.

[MaxOstrowski]

Thanks for your feedback. I know that the given example is cubic, but there exist a lot of examples with only 2 predicates (quadratic). Do you think it is still a good idea to do this translation in general ? So also for 2 predicates ? @rkaminsk

[rkaminsk]

Thanks for your feedback. I know that the given example is cubic, but there exist a lot of examples with only 2 predicates (quadratic). Do you think it is still a good idea to do this translation in general ? So also for 2 predicates ? @rkaminsk

It should be a relatively safe thing to do. For large domains it is likely to pay off. For smaller to medium size domains it might be nice to have constraints in clasp's binary constraint graph. In the end, one has to benchmark this anyway...

[MaxOstrowski]

I think I would need a little bit of help. I started working on this and #56 on https://github.com/potassco/ngo/tree/issue/56

The translation to count aggregates from these symmetries in normal rules already works with some restrictions. Within aggregates this seems to be a bit more complicated (currently i produce this nice but invalid AST)

2 <= #count { W: match(_,W), 3 <= #count { M1: match(M1,W) } }.

As this needs to be solved more generally, and global variables may need binding these are my currents thoughts:

INPUT:

head(H1, ..., Hn) :- body(H1, ..., Hn, B1, ..., Bn), Bi ~ #count{ W : agg(Hi, Bj,A1,W), agg(Hi,Bj,A2,W), A1 != A2}.

I thought about moving the count aggregate to another rule and first compute the inner at least two constraint. Something like:

aux(H1, ..., Hn, Bi, W) :- body(H1, ..., Hn, B1, ..., Bn), 2 <= #count{ A : agg(Hi, Bj,A,W), agg(Hi,Bj,A,W)}, agg(_,_,_,W).
head(H1, ..., Hn) :- Bi ~ #count{  W : aux(H1, ..., Hn, Bi, W) }, aux(H1, ..., Hn, Bi, _).

This does not look like much of an improvement, no ? Do you have any idea on this ? @rkaminsk

[rkaminsk]

I think that this could be approached as follows:

You order the body literals in a safe rule

$$h \leftarrow b_1 \wedge \ldots \wedge b_n$$

in such away that $\{b_1,\ldots,b_n\} = \{c_1,\ldots,c_n\}$ and

$$\bot \leftarrow c_1 \wedge \ldots \wedge c_i$$

is safe for all $i \leq n$.

From there one can introduce a auxiliary predicates for aggregate elements. The trick is to have a good ordering heuristic and a good heuristic to guess when this is worthwhile. For example if $c_i$ is an aggregate, you can add all $c_j$ with $j \lt i$ to the conditions to obtain a set of literals that can be used as a body of an auxiliary rule.

[MaxOstrowski]

So the idea would be to put as less body literals as possible into the original rule while it still being safe and put all the rest in the new aux rule. This is similar to what I tried to describe above but simply using all body literals in the aux rule and using the aux predicate to make the original rule safe again. I`ll look into your proposal and see what it makes with same examples, thank you.