我们能否在具有一系列值的 ForAll 量词下使用一些变量来解决 Z3 中的一组约束？

Question

我想解决一组约束如下：

C1: x1 > x2
C2: y1 = x1 + t1
C3: y2 = x2 + t2
C4: 2 <= t1 <= 7
C5: 5 <= t2 <= 9
C6: x1 >= 0
C7: x2 >= 0
C8: y1 < y2

如果我在 Z3 中正常检查这个，它会提供一个令人满意的解决方案。但我想知道对于 t1 和 t2 的所有值，约束集是否为真。

如何在 Z3 或任何其他 SMT 求解器中对其建模？

Answer 1

你的问题比较含糊，因为它可以解释为不同的意思。但我了解到您正在尝试确定是否存在可以违反这些约束的含义的值？也就是说，在您的示例中，是否有一种方法可以选择 C1-C7 都满足但 C8 不满足的值？

如果是这种情况，那么通常的技巧是从您的约束条件所呈现的其他事实中确定您想要遵循的事实。然后，你断言结论的否定。如果否定是不可满足的，那么你的约束对所有可能的赋值都是有效的。但是，如果你得到 unsat，则意味着没有反例，即你的约束对所有可能的赋值都有效。

对于您的情况，我认为 C1-C7 是 "given"，而 C8 是您要建立的。您只需声明所有 C1-C7，但否定 C8。在下文中，我假设变量是整数值：

(set-logic ALL)
(set-option :produce-models true)

(declare-fun x1 () Int)
(declare-fun x2 () Int)
(declare-fun y1 () Int)
(declare-fun y2 () Int)
(declare-fun t1 () Int)
(declare-fun t2 () Int)

(assert (> x1 x2))        ; C1
(assert (= y1 (+ x1 t1))) ; C2
(assert (= y2 (+ x2 t2))) ; C3
(assert (<= 2 t1 7))      ; C4
(assert (<= 5 t2 9))      ; C5
(assert (>= x1 0))        ; C6
(assert (>= x2 0))        ; C7

(assert (not (< y1 y2)))  ; NEGATION of C8

(check-sat)
(get-value (x1 x2 t1 t2 y1 y2))

当运行时，z3 表示：

sat
((x1 1)
 (x2 0)
 (t1 4)
 (t2 5)
 (y1 5)
 (y2 5))

好了，好了。您的约束对上述选择无效，您可以轻松验证自己。

这是您要找的吗？

我们能否在具有一系列值的 ForAll 量词下使用一些变量来解决 Z3 中的一组约束？

Can we solve a set of constraints in Z3 with some variables under ForAll quantifier having a range of values?

z3

smt

quantifiers

first-order-logic