-1

我正在寻找一种工具来确定给定的一组线性方程/不等式 (A) 是否需要另一组给定的线性方程/不等式 (B)。返回值应该是“真”或“假”。

为了说明，让我们看一下 A 和 B 的可能实例以及算法的预期返回值：

A: {Z=3,Y=Z+2, X < Y} ;
B: {X<5} ; 
Expected result: true

A: {Z=3,Y=Z+2, X < Y} ;
B: {X<10} ;
Expected result: true

A: {Z=3,Y=Z+2, X < Y} ;
B: {X=3} ; 
Expected result: false

A: {X<=Y,X>=Y} ;
B: {X=Y} ; 
Expected result: true

A: {X<=Y,X>=Y} ;
B: {X=Y, X>Z+2} ; 
Expected result: false

通常 A 包含多达 10 个方程/不等式，B 包含 1 或 2 个。它们都是线性的并且相对简单。我们甚至可以假设所有变量都是整数。

这个任务 - 确定 A 是否需要 B - 是更大系统的一部分，因此我正在寻找已经实现了类似的东西并且我可以使用的工具/源代码/包。

我开始看的东西：

  1. 代数定理证明器 - Otter、EQP 和 Z3（Vampire 目前无法下载）。
  2. Coq 正式的证明管理系统。
  3. 线性规划。

但是，我使用这些工具的经验非常有限，到目前为止我还没有找到有希望的方向。任何比我更有经验的人的指导和想法都将受到高度赞赏。

感谢您的时间！

4

1 回答 1

0

我想我找到了一个可行的解决方案。该问题可以重新表述为分配问题，然后可以通过定理证明器（例如 Z3）来解决，并且可能还可以通过线性规划求解器进行一些工作。

为了说明，让我们看一下我上面给出的第一个例子：

A: {Z=3, Y=Z+2, X<Y} ;
B: {X<5} ;

判断 A 是否蕴含 B 等价于判断 A 是否为真而 B 为假是不可能的。这是一个简单的逻辑等价。在我们的例子中，这意味着不是检查 B 中的条件是否遵循 A 中的条件，而是检查是否存在满足 A 中而不是 B 中的条件的 X、Y 和 Z 的赋值。

现在，当被表述为分配问题时，可以为该任务调用诸如 Z3 之类的定理证明器。以下代码检查 A 中的条件是否满足，而 B 中的条件不满足：

(declare-fun x () Int)
(declare-fun y () Int)
(declare-fun z () Int)
(assert (= z 3))
(assert (= y (+ z 2))) 
(assert (< x y))
(assert (not (< x 5)))
(check-sat)
(get-model)
(exit)

Z3 报告没有满足这些条件的模型，因此 B 不可能不遵循 A，因此我们可以得出结论 B 遵循 A。

于 2016-02-11T23:44:41.533 回答