求解（多于两个）线性不等式的系统答案

【问题标题】：Solving a system of (more than two) linear inequalities求解（多于两个）线性不等式的系统
【发布时间】：2017-03-09 06:50:24
【问题描述】：

如果我使用

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])

我明白了：

NotImplementedError: 
inequality has more than one symbol of interest

sympy、sage、prolog、haskell 或其他一些可免费获得的产品是否具有解决以这种方式出现的线性不等式系统的方法。

谢谢！

【问题讨论】：

你看docs.sympy.org/latest/modules/solvers/…了吗？我从未尝试过，但似乎它应该适用于线性不等式。如果数字解决方案足够，请查看scipy.optimize.linprog()。
您能否发布一个您想求解的方程类型的示例。
非常感谢@Dietrich 的评论。在遇到stackoverflow.com/questions/40441532/… 的问题之前，我一直忘记阅读它。我不明白有可能解决系统的不等式。
@Dietrich：显然 reduce_inequalities 不能处理多个符号。
@asmeurer：感谢您的回复。我已经包含了丢番图方程。

标签： haskell prolog sympy sage inequalities

【解决方案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 在 0..sup, 2*X+3*Y#=5*Z+77, Y 在 0..sup 中， Z 在 0..sup.

根据要求，此附加目标将变量限制为非负整数。系统的回答仍然没有多大帮助。

您可以使用label/1 搜索具体的解决方案。但是，这种所谓的标签要求所有域都是有限，因此我们目前得到：

?- 2*X + 3*Y - 5*Z #= 77, Vs = [X,Y,Z], VS ins 0..sup, 标签（Vs）。 错误：参数没有充分实例化

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

?- 2*X + 3*Y - 5*Z #= 77, Vs = [X,Y,Z], Vs ins 0..10 000 000 000 000 000 000, 标签（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) 可能也值得一试。

【讨论】：