Z3 表示如果 a^3=x*y*z 则 3a <= x+y+z

Question

我是 Z3 的新手（从今天开始）。至今非常喜欢。很棒的工具。不幸的是，语法让我有点困惑。

我想证明如果：

a^3 = xyz = m (with a, x, y, z, m (0..1) )

那么：

3a

我通过尝试找到满足以下条件的模型来做到这一点：

3a > (x+y+z)

这是 Z3 代码：

(declare-const a Real)
(declare-const x Real)
(declare-const y Real)
(declare-const z Real)
(declare-const m Real)

(assert (> a 0))
(assert (< a 1))
(assert (> x 0))
(assert (< x 1))
(assert (> y 0))
(assert (< y 1))
(assert (> z 0))
(assert (< z 1))
(assert (> m 0))
(assert (< m 1))

(assert (= (* (* a a) a) m))
(assert (= (* (* x y) z) m))
(assert (> (* 3.0 a) (+ (+ z y) x) ))
(check-sat)

模型不满意。

我是否成功证明了我想要的？正如我所说，语法让我感到困惑，因为我是个新手。

Answer 1

你的解决方案是正确的。

说明：你写的等价于：

0 < x < 1
0 < y < 1
0 < z < 1
0 < m < 1
a * a * a = m
x * y * z = m
3 * a > x + y + z

Z3 说这是无法满足的。因此，如果

a^3 = xyz = m (with a, x, y, z, m (0..1) )

那么不可能是这样的：

3a > (x+y+z)

因为，如果确实发生了这种情况，那么您提出的 SMT 问题将是可满足的，这与 Z3 声称 SMT 问题不可满足的说法相矛盾。如果不是3a > (x+y+z)，那么一定是3a <= (x+y+z)，这就是你原本要证明的陈述。

Answer 2

我认为您的解决方案是正确的。让我解释一下使用 Z3 来证明声明 A 的有效性。关键思想是，在经典逻辑中，例如命题逻辑和谓词逻辑：

• A 有效当且仅当 negation(A) 无法满足。

这是一个众所周知的结果。您可以在许多教科书和资料中找到它，例如，在this slide 的第 4 页。因此，P -> Q 的有效性可以通过检查其否定的不可满足性来证明：P /\ negation(Q)。

特别是，对于你的例子，

(a^3 = x*y*z = m) -> (3a <= x+y+z) 有效，

如果

(a^3 = m) /\ (x*y*z = m) /\ (3a > x+y+z) 无法满足。