我想解决如下一组约束：
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 求解器中建模？
【问题讨论】：
标签： z3 smt quantifiers first-order-logic
您的问题相当含糊，因为它可以解释为不同的意思。但我猜你是想确定是否存在可能违反这些约束含义的值？也就是说，在您的示例中，有没有办法选择 C1-C7 都满足但 C8 不满足的值？
如果是这种情况，那么通常的技巧是从您的约束存在的其他事实中确定您想要遵循的事实。然后，你断言结论的否定。如果否定是不可满足的，那么您的约束对所有可能的分配都是有效的。但是，如果您得到unsat，则意味着没有反例，即您的约束对所有可能的分配都有效。
在您的情况下，我认为 C1-C7 是“给定的”，而 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))
那么，就这样吧。您的约束不适用于上述选择，因为您可以轻松验证自己。
这是你要找的吗？
【讨论】：