z3 - 包含约束

Question

给定非负实数tSS, tLS, tIS, tBS。（即它们是实型，tSS>=0 且 tLS>=0 且 tIS>=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，反之则不然。ae 的值是从 0 到无穷大的值。无穷大意味着它可以取任何大于 0 的值。

是否可以使用Z3来推断ae的值？（可能无法满足）

Answer 1

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

让C1(tSS, tLS, tIS, tBS)表示 CNF 公式，并且C2(SS, tLS, tIS, tBS, a, b, c, d)是要满足的约束。您可以检查以下量化公式的可满足性：

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

哪里a, b, c, d是自由变量。

我使用 Z3 SMT online对您的具体示例进行了编码。在这种情况下，查询是不可满足的。