包含约束

Question

给定非负实数tSS, tLS, tIS, tBS。（即，它们是实型，tSS>=0，tLS>=0，tSS>>=0，tBS>=0，tSS>=0）

下面的约束C1是CNF格式，包含12个连词。

(tSS+tLS<=tIS)And(tIS<=tBS)And(tSS+tLS+tIS+tBS<=3) OR
(tSS+tLS<=tBS)And(tBS<=tIS)And(tSS+tLS+tIS+tBS<=3) OR
(tSS+tLS<=tBS)And(tSS<=tIS)And(tIS<=tSS+tLS)And(tSS+tLS+tIS+tBS<=3) OR
(tSS<=tIS)And(tIS<=tBS)And(tBS<=tSS+tLS)And(tSS+tLS+tIS+tBS<=3) OR
(tSS+tLS<=tIS)And(tSS<=tBS)And(tBS<=tSS+tLS)And(tSS+tLS+tIS+tBS<=3) OR
(tSS<=tBS)And(tBS<=tIS)And(tIS<=tSS+tLS)And(tSS+tLS+tIS+tBS<=3) OR
(tSS+tLS<=tBS)And(tIS<=tSS)And(tSS+tLS+tIS+tBS<=3) OR
(tSS<=tBS)And(tIS<=tBS)And(tBS<=tSS+tLS)And(tSS+tLS+tIS+tBS<=3) OR
(tIS<=tBS)And(tBS<=tSS)And(tSS+tLS+tIS+tBS<=3) OR
(tSS+tLS<=tIS)And(tBS<=tSS)And(tSS+tLS+tIS+tBS<=3) OR
(tSS<=tIS)And(tBS<=tSS)And(tIS<=tSS+tLS)And(tSS+tLS+tIS+tBS<=3) OR
(tIS<=tSS)And(tBS<=tIS)And(tSS+tLS+tIS+tBS<=3)

我希望以的形式获得约束C2

tSS<=a and tLS<=b and tIS<=c and tBS <=d and tSS<=e

约束C2只需要包含在C1中，即。满足C2的任何估值都必须满足C1，但不能反之亦然。a-e的值是从0到无穷大范围内的值。无穷大意味着它可以取任何大于0的值。

是否可以使用Z3来推断a-e的值？（可能不令人满意）

Answer 1

可能有更有效的技术可以做到这一点，但至少可以使用量词来解决问题。

设CCD_ 2表示CNF公式，CCD_。您可以检查以下量化公式的可满足性：

forall tSS tLS tIS tBS. C2(SS, tLS, tIS, tBS, a, b, c, d) => C1(tSS, tLS, tIS, tBS)

其中CCD_ 5是自由变量。

我在线使用Z3SMT对您的具体示例进行了编码。在这种情况下，查询是不令人满意的。