3

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!

Bill Bell
  • 21,021
  • 5
  • 43
  • 58
  • Did you look at http://docs.sympy.org/latest/modules/solvers/inequalities.html#inequality-docs ? I never tried it, but seems it should work for linear set of inequalities. If numeric solutions suffice, take a look at `scipy.optimize.linprog()`. – Dietrich Oct 31 '16 at 21:12
  • Can you please post an example of the type of equation you would like to solve. – asmeurer Nov 01 '16 at 19:13
  • Many thanks to @Dietrich for your comment. I had been forgetting to read it until I encountered the question at http://stackoverflow.com/questions/40441532/how-to-restrict-sympy-finiteset-containing-symbol/40443339#40443339. I hadn't understood that it's possible to solve *systems* of inequalities. – Bill Bell Nov 05 '16 at 21:24
  • @Dietrich: Apparently reduce_inequalities can't handle more than one symbol. – Bill Bell Nov 05 '16 at 22:30
  • @asmeurer: Thanks for responding. I've included the Diophantine equation. – Bill Bell Nov 05 '16 at 22:31

1 Answers1

3

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 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.

mat
  • 40,498
  • 3
  • 51
  • 78