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:
 WITH N<A
 WITH N<B
 WITH N<C
 WITH A*B=P*C+N
 WITH A*C=Q*B+N
 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:
 C<=A,  C<=B, and  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:
therefore  A divides 12*Q+12*C.
From constraints 5 and 8, one has Q*B<A*C<=A*B, therefore  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  7*A=12*Q+12*C.
Removing A from constraints13 and 4, one gets:
As constraint 5 can be written: Q*B=A*C-12, one has:
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.
2 thoughts on “II. Symmetries help to solve the problem”
Is there any way for the reader to reproduce that interesting experiment? In other words, is the CAIA software system described here available (e.g. as some caia*.tar.gz tar archive file, or on some github repository, or whatever) with instructions detailed enough to reproduce that run? I believe that even if CAIA is buggy and imperfect, it is worth the effort to publish it as some experimental free software and many AI researchers are doing that. BTW, the current facilities available on the web (e.g. github) makes that easy to do.
This is a very good idea. Unfortunately, I have a huge Todo list; most of its elements are more important for bootstrapping AI. It will have to wait!
Moreover, I already did it nine years ago, for an older version of CAIA; it does not seem that many people were interested.
One can still find it at: