Questions about solving integer constraints in CLP

Question

I'm working on a constraint solver for finite set theory known as {log} ('setlog'). For some reasons {log} formulas allow integer constraints. So far {log} rests on CLP(FD) for solving those constraints. However, we need more; in particular, we need to get rid of binding a finite domain for all integer variables. In other words, we need some CLP system making a more abstract reasoning over the integers.

We are trying CLP(Q,R). It comes with this bb_inf/4 predicate which can search for integer solutions of systems of linear equalities and disequalities. This would be fine but it's not complete. For example it fails to find the right answer for the following system:

3*X + 5*Y + 6*Z = 6

X + 3*Y - 2*Z = 5

where X, Y and Z are integer variables. This system has no integer solutions, although it has an infinite number of rational/real solutions. On the other hand, CLP(Q,R) finds the correct answer for this system (which is equal to the one above except that 7 goes instead of 6 in the first equation):

3*X + 5*Y + 6*Z = 7

X + 3*Y - 2*Z = 5

this system has infinitely many integer solutions.

Then, we wonder whether there are CLP systems implementing:

• some linear integer programming algorithm to solve systems of linear equalities and disequalities; and/or

• some method to solve systems of linear Diophantine equations

All the best, Maxi

Answer 1

CLP(FD) and CLP(Z) constraints work by constraint propagation. This is somewhat different than the simplex method and other approaches that are applied for CLP(Q).

In the case of CLP(Z), we are faced with the situation that we know from Matiyasevich's theorem that no propagation mechanism can ever be complete in the sense that it:

• always terminates
• and correctly determines whether a system of Diophantine equations has a solution.

For this reason, CLP(Z) systems are called incomplete: You need an explicit search for solutions.

The good news is that you can of course perform the search! However, CLP(Z) only allows you to start the search if the search space is finite. So, if you are searching for concrete solutions, one strategy is to use iterative deepening, where you try increasingly larger intervals. For example:

?- 3*X + 5*Y + 6*Z #= T,
   T #= 7*X + 3*Y - 2*Z,
   T #= 5,
   Vs = [X,Y,Z],
   length(_, Upper),
   Lower #= -Upper,
   Vs ins Lower..Upper,
   label(Vs).

The first three lines are the equations from your example. The rest of the query performs the search, using increasingly larger yet always finite intervals starting with 0..0, -1..1, -2..2, etc. on backtracking. This is a complete search strategy, with the drawback that it may not terminate.

Here is one concrete solution:

X = Z, Z = -5,
Y = Upper, Upper = 10,
T = 5,
Vs = [-5, 10, -5],
Lower = -10 ;

You can append portray_clause(Vs), false to the query to force backtracking, yielding:

[-5, 10, -5].
[-5, 10, -5].
[-5, 10, -5].
[-5, 10, -5].
[-5, 10, -5].
[9, -14, 8].

Thus, we have already found two solutions. Some of them are reported redundantly.

Linear equalities, disequalities, and also many other types of constraints can be handled by CLP(Z)! Note though that if there are no solutions, then this approach will never terminate, not even existentially.

CLP(Q) (if you have a system where it works) can be used to complement CLP(Z), for example as follows: If CLP(Q) fails, then you know there is no solution in Q and hence also not in Z.

Here is an example from your comments:

?- { X > Y, Y > X }.
false.

We have thus used CLP(Q) to prove the absence of solutions in Z.

All considered, CLP(Z) is a good approach to tackle integer equations, but you will likely need to combine it with more approaches to get the most out of it, such as CLP(Q) and specialized reasoning over particular fragments. See for example Presburger arithmetic, which is consistent, complete and also decidable.