haskell - 求解(两个以上)线性不等式系统

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

我得到:

NotImplementedError: 
inequality has more than one symbol of interest

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

谢谢!

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).ERROR: Arguments are not sufficiently instantiated

好消息(在某​​种意义上)是我们没有时间在任何情况下都尝试所有 可能性。所以我们不妨将自己限制在搜索空间的某个有限部分。例如:

?- 2*X + 3*Y - 5*Z #= 77,   Vs = [X,Y,Z],   Vs ins 0..10 000 000 000 000 000 000,   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] ;etc.

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