Solving a system of (more than two) linear inequal

Question

If I use

diophantine(2*x+3*y-5*z-77)

I receive this result.

{(t_0, -9*t_0 - 5*t_1 + 154, -5*t_0 - 3*t_1 + 77)}

Fine so far. However, on occasion one might like to constrain x, y and z to be (say) non-negative. When I use an approach like this<

reduce_inequalities([0<=t_0, 0<=-9*t_0 - 5*t_1 + 154, 0<=-5*t_0 - 3*t_1 + 77],[t_0, t_1])

I get:

NotImplementedError: 
inequality has more than one symbol of interest

Does sympy, sage, prolog, haskell or some other freely available product have means for solving systems of linear inequalities that arise in this way.

Thank you!

Answer 1

To reason about integers in Prolog, you can use your Prolog system's CLP(FD) constraints.

The exact details differ slightly between different Prolog systems. Please see your system's manual for more information, and also clpfd for related questions.

In your case, we can start by simply posting the constraint:

?- 2*X + 3*Y - 5*Z #= 77.
2*X+3*Y#=5*Z+77.

In this case, and as for all pure Prolog programs, the system's answer is declaratively equivalent to the original query. This does not help a lot here: The system has only slightly rewritten the original constraint.

You can constrain this further, for example with:

?- 2*X + 3*Y - 5*Z #= 77,
   [X,Y,Z] ins 0..sup.
X in 0..sup,
2*X+3*Y#=5*Z+77,
Y in 0..sup,
Z in 0..sup.

As requested, this additional goal constrains the variables to non-negative integers. The system's answer still does not help a lot.

You can use label/1 to search for concrete solutions. However, this so-called labeling requires that all domains be finite, and so we currently get:

?- 2*X + 3*Y - 5*Z #= 77,
   Vs = [X,Y,Z],
   Vs ins 0..sup,
   label(Vs).
ERROR: Arguments are not sufficiently instantiated

The good news (in a sense) is that we don't have time to try all possibilities in any case. So we might as well restrict ourselves to some finite part of the search space. For example:

?- 2*X + 3*Y - 5*Z #= 77,
   Vs = [X,Y,Z],
   Vs ins 0..10 000 000 000 000 000 000,
   label(Vs).

With this query, you get concrete integers as solutions:

X = 0,
Y = 29,
Z = 2,
Vs = [0, 29, 2] ;
X = 0,
Y = 34,
Z = 5,
Vs = [0, 34, 5] ;
X = 0,
Y = 39,
Z = 8,
Vs = [0, 39, 8] ;
X = 0,
Y = 44,
Z = 11,
Vs = [0, 44, 11] ;
etc.

Since you are reasoning over linear constraints, CLP(Q) may also be worth a try.