The solution of a problem often depends upon a set of variables, whose all possible values are known; the combinatorial search considers which combinations of these values satisfy all the constraints of the problem. This can also be used when there is a finite number of legal actions, and one considers the situations after all the legal sequences of these actions. This search is widely used in AI, for instance for chess programs. It frequently gives useful results: with their speed, the computers can develop trees much larger than those that we could ever generate.
However, even when this method succeeds, we are not satisfied: the only way to understand a solution found in that way is to know that everything has been considered, and one has found nothing else. We cannot check such solutions. Moreover, it cannot be used when the search space is very large, and always when there is an infinite number of values; this often happens in solving arithmetic problems.
Instead of considering all the possible values for each variable, one can also consider a combination of the rules that can create new constraints, enriching the formulation of the problem. In many cases, the new problem may become very easy to solve.
In order to clarify this idea, let us consider how CAIA solves a particular arithmetic problem: to find all the integers m and n satisfying the equation 4m+3n2=34 .
One cannot use the combinatorial search, there are an infinity of possible values for m and n. Here is CAIA’s solution:
3n2 is the difference of two even numbers, so it is even.
As 3n2 is even, and 3 is odd, n2 is even.
Therefore n est even.
Then n2 is a multiple of 4,
and 3n2 is a multiple of 4.
So, 4m+3n2 is a multiple of 4.
As it must be equal to 34, which is not a multiple of 4, there is a contradiction: no solution.
Naturally, at each step, CAIA must find and apply an element of its set of rules, for instance: in an equation, if a member is a multiple of integer I, then the other member is also a multiple of I. Another useful rule is: the sum of two expressions that are multiple of integer I is also a multiple of I.
A huge advantage of the meta-combinatorial search over the combinatorial one is that one has not to consider all the possible applications of the rules: one has only to find a sequence that leads to the solution. Many other rules were perhaps considered; if they are not necessary for the proof, it is useless to indicate that one attempted to use them. For instance, it happened that CAIA found that, as the square n2 is a positive or null integer, this is also true for 3n2. Therefore, 4m=34-3n2<=34, and m<9. I do not included this result in the preceding proof, the contradiction has been proved without using it.
The combinatorial search could be used in a variant of this problem where the absolute values of both m and n are less than one billion. Then, one can consider all the possible values of n, and check that 34-3n2 is a multiple of 4. A lot of time would be wasted to find that there is no solution. Proving first that n is even and m<9 would reduce the size of the search space. Indeed, it is often interesting to use both kinds of search: the meta-combinatorial search trims down the problem, then the combinatorial search solves when the size of the search space is reasonable. We will show in future posts how CAIA manages to use both methods.
The mathematician frequently uses a meta-combinatorial search. He may spend years finding the proof of a theorem, writing notebook after notebook, when the final solution takes only a few pages.
When our AI systems will have many methods for enriching the formulation of problems, they will efficiently use the meta-combinatorial search. Some day, the mathematicians will be as surprised as the chess players were some years ago: during many years, they were laughing at the poor performances of the programs, and at their ridiculous moves. For the present time, they are reduced to demand that their artificial opponent will be shackled by the interdiction to use all its capacities; this does not prevent them to lose.