Sometimes, finding symmetries enable CAIA to solve problems that it could not solve otherwise. In particular, this happens when a proof by cases is necessary. We will try to illustrate that with a family of problems, called TRIPLETS. For these problems, one must find three positive integers A, B, and C, such that the remainder of the division of the product from two of these numbers by the third one is always the integer N. This problem is formulated for CAIA in the following way:

LET CTE N

LET SET E=[1 to PLINF]

(PLINF stands for plus infinite)

FIND VARIABLE A IN E

followed by 5 similar orders for variables B, C, P, Q, R. Finally, we have the six following constraints:

[1] WITH N<A

[2] WITH N<B

[3] WITH N<C

[4] WITH A*B=P*C+N

[5] WITH A*C=Q*B+N

[6] WITH B*C=R*A+N

Giving the value of N defines one of the problems of the family, N=12 for the present example.

CAIA looks for the symmetries in this formulation, and it finds 5 of them: A, B, C corresponds to the five other permutations of these three variables: A, C, B and B, A, C and B, C, A and C, A, B and C, B, A. To avoid to generate symmetrical solutions, CAIA adds the three following constraints:

[7] C<=A, [8] C<=B, and [9] B<=A.

In that way, it defines one case of a proof by case: the values of the other cases are automatically defined by the five symmetries. Contrarily to what happens in usual proofs by case, it is sufficient to solve one case.

Then CAIA solves a particular problem, here N=12. I will only give the critical steps of the proof. Eliminating B from constraints 5 and 6, one has:

[10] A*C²=A*R*Q+12*Q+12*C

therefore [11] A divides 12*Q+12*C.

From constraints 5 and 8, one has Q*B<A*C<=A*B, therefore [12] Q<A. From 12 and 7, one finds 12*Q+12*C<24*A. As, from 11, A divides 12*Q+12*C less than 24*A, there are only 23 possibilities:

A=12*Q+12*C or 2*A=12*Q+12*C…..or 22*A=12*Q+12*C or 23*A=12*Q+12*C

After that, CAIA develops 23 branches of the tree, each with one of the preceding constraints. For some of them, there is no solution, for others one or more solutions. This step could be made only with constraints 8 and 7, added for avoiding to generate symmetrical solutions. Without them, CAIA finds constraint 11, but cannot use it; finally, it stops without finding any solution.

Let us consider what happens in one of these branches, for instance when on add constraint [13] 7*A=12*Q+12*C.

Removing A from constraints13 and 4, one gets:

[14] 12*Q*B+12*C*B=7*C*P+84

As constraint 5 can be written: Q*B=A*C-12, one has:

[15] 12*A*C+12*C*B=7*C*P+228

Therefore C divides 228. As C>12, it has one of the following values:

19, 38, 57, 76,114, 228

That makes six new branches for the tree, and CAIA easily finds solutions or contradictions for each of them.

All in all, the tree has 218 leaves. 132 of them are solutions, for instance: A=24, B=18, and C=14, or A=293,892, B=1884, and C=156.

We can check that A*B=293,892*1884=553,692,528=P*C+12=3,549,311*156+12, and the same verifications for B*C and C*A.

With the symmetries, there are 132*6= 792 solutions. One must not consider the other cases, they are already solved since they correspond to symmetrical solutions. Symmetries are very useful when they define a proof by cases: it is sufficient to solve one of them.

The constraints created for avoiding to generate symmetrical solutions have been used twice for proving the key constraint: 12*Q+12*C<24*A. If CAIA does not look for the symmetries, it is not even able to find one of the 792 solutions.