约束比较器

Question

您知道我可以用来比较约束条件的工具吗(不仅是数学方面的)？用例子更容易解释:

A)简单的例子

C1: x < 0 && y * y < x
C2: x < 0 && y * y < x - 1

我想知道 C2 是否比 C1 强，确实如此。也就是说，C2 的 (x,y) 也在 C1 中。

B)复杂的例子

C1: x > 0 && y > 0
C2: x > 0

C2 比 C1 弱，因为它不包含对 y 的约束。

我可以尝试手写一些东西，但我认为这不是解决方案。我知道解决约束的问题是不可判定的，但我想知道在这个方向上做了哪些工作。

谢谢，

Answer 1

您是否正在尝试确定约束 C1 是否包含 C2(这意味着不可能找到一组满足 C1 且不满足 C2 的值 -> C2 在所有 C1 为真但可能不为真的场景中为真另一种方式)？。当 C1 包含 C2 时，可以删除 C2，因为它不会为问题添加任何语义。

如果是这种情况，我建议您为此使用 CSP 求解器。这比看起来容易。例如，Eclipse CSP 求解器(这里的 Eclipse 不是指 IDE 平台，求解器具有相同的名称)可以通过定义良好的 API 从您的 Java 程序中轻松调用，因此您可以将问题发送给求解器，然后看看哪个约束更弱