解决一个包含（两个以上）线性不等式的系统

Question

如果我使用

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

我收到了这个结果。

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

目前为止还不错。然而，有时候我们可能希望限制 x、y 和 z 为（比如说）非负数。当我使用这种方法时<

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

请问Sympy、Sage、Prolog、Haskell或其他免费产品是否有解决线性不等式系统的方法呢？

谢谢！

- Bill Bell

---

你看过 http://docs.sympy.org/latest/modules/solvers/inequalities.html#inequality-docs 吗？我从未尝试过，但似乎它应该适用于线性不等式组。如果数值解足够，可以看看 scipy.optimize.linprog()。 - Dietrich

你能否请提供一个您想解决的方程类型的例子。 - asmeurer

非常感谢@Dietrich的评论。在遇到https://dev59.com/KZzha4cB1Zd3GeqPCD-f#40443339上的问题之前，我一直忘记去阅读它。我之前并没有理解解决*不等式系统*是可能的。 - Bill Bell

@Dietrich：显然，reduce_inequalities无法处理多个符号。 - Bill Bell

@asmeurer：感谢您的回复。我已经包含了丢番图方程。 - Bill Bell

Answer 1

要在Prolog中推理关于整数的问题，您可以使用Prolog系统的CLP(FD)约束。

不同的Prolog系统之间确切的细节略有不同。有关更多信息，请参阅您系统的手册，以及相关问题的clpfd。

在您的情况下，我们可以通过简单地发布约束条件来开始：

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

在这种情况下，对于所有纯Prolog程序，系统的答案在声明上与原始查询是等价的。这在这里并没有帮助：系统只是稍微重新编写了原始约束。

您可以进一步限制这个问题，例如：

?- 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.
作为要求，这个附加目标将变量限制为非负整数。系统的答案仍然不是很有帮助。
您可以使用label/1搜索具体解决方案。但是，这种所谓的标记需要所有域都是有限的，因此我们当前得到：
?- 2*X + 3*Y - 5*Z #= 77,
   Vs = [X,Y,Z],
   Vs ins 0..sup,
   label(Vs).
错误：参数未充分实例化

好消息（在某种意义上）是我们无论如何都没有时间尝试所有可能性。所以我们最好将自己限制在搜索空间的一部分。例如：

使用以下查询，您可以获得具体的整数解决方案：

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] ;
等等。

由于您正在对线性约束进行推理，因此CLP(Q)也值得一试。

- mat