关于在 CLP 中求解整数约束的问题

Question

我正在研究一种称为 {log} ('setlog') 的有限集理论的约束求解器。由于某些原因，{log} 公式允许整数约束。到目前为止，{log} 依赖于 CLP(FD) 来解决这些约束。但是，我们需要更多；特别是，我们需要摆脱绑定所有整数变量的有限域。换句话说，我们需要一些 CLP 系统对整数进行更抽象的推理。

我们正在尝试 CLP(Q,R)。它带有这个 bb_inf/4 谓词，可以搜索线性等式和不等式系统的整数解。这很好，但它并不完整。例如，它无法为以下系统找到正确答案：

3*X + 5*Y + 6*Z = 6

X + 3*Y - 2*Z = 5

其中 X、Y 和 Z 是整数变量。这个系统没有整数解，尽管它有无数个有理/实数解。另一方面，CLP(Q,R) 找到了这个系统的正确答案（除了第一个方程中的 7 代替 6 之外，它等于上面的那个）：

3*X + 5*Y + 6*Z = 7

X + 3*Y - 2*Z = 5

这个系统有无穷多个整数解。

然后，我们想知道是否有 CLP 系统实现：

• 一些线性整数规划算法，用于求解线性等式和不等式系统；和/或

• 求解线性丢番图方程组的一些方法

一切顺利， 马克西

Answer 1

CLP(FD) 和 CLP(Z) 约束通过约束传播起作用。这与应用于 CLP(Q) 的单纯形法和其他方法有些不同。

在 CLP(Z) 的情况下，我们面临从Matiyasevich's theorem 了解到的情况，即没有传播机制 永远不可能是完整的它：

• 总是终止
• 和正确判断丢番图方程组是否有解。

出于这个原因，CLP(Z) 系统被称为不完整：您需要明确的搜索解决方案。

好消息是您当然可以执行搜索！但是，CLP(Z) 只允许您在搜索空间为有限 时开始搜索。因此，如果您正在寻找具体的解决方案，一种策略是使用迭代深化，您可以尝试越来越大的间隔。例如：

?- 3*X + 5*Y + 6*Z #= T, T #= 7*X + 3*Y - 2*Z, T #= 5， Vs = [X,Y,Z], 长度（_，上）， 下#= -上， VS 下层..上层， 标签（Vs）。

前三行是您示例中的方程式。查询的其余部分执行搜索，使用越来越大但始终有限的间隔，从 0..0、-1..1、-2..2 等开始回溯。这是一个完整的搜索策略，缺点是它可能不会终止。

这是一个具体的解决方案：

X = Z，Z = -5， Y = 上，上 = 10， T = 5, Vs = [-5, 10, -5], 下 = -10 ;

您可以将portray_clause(Vs), false 附加到查询以强制回溯，产生：

[-5、10、-5]。 [-5、10、-5]。 [-5、10、-5]。 [-5、10、-5]。 [-5、10、-5]。 [9, -14, 8]。

因此，我们已经找到了两个解决方案。其中一些是多余的报告。

CLP(Z) 可以处理线性等式、不等式以及许多其他类型的约束！请注意，如果没有解决方案，那么这种方法将永远不会终止，甚至不会存在。

CLP(Q)（如果你有一个可以运行的系统）可以用来补充 CLP(Z)，例如如下：如果 CLP(Q) 失败，那么你知道 Q 中没有解决方案 因此也不在 Z 中。

这是来自您的 cmets 的示例：

?- { X > Y, Y > X }。 错误。

因此，我们使用 CLP(Q) 来证明 Z 中不存在解。

综合考虑，CLP(Z) 是处理整数方程的好方法，但您可能需要将其与更多方法结合使用以充分利用它，例如 CLP(Q) 和对特定片段的专门推理.参见例如Presburger arithmetic，它是一致的、完整的并且是可判定的。