Z3 表明如果 a^3=x*y*z 那么 3a <= x+y+z [英] Z3 to show that if a^3=x*y*z then 3a &lt;= x+y+z

问题描述

我是 Z3 的新手(从今天开始).到目前为止非常喜欢它.很棒的工具.不幸的是，语法让我有点困惑.

我想证明如果:

<块引用>

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

然后:

<块引用>

3a <= (x+y+z)

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

<块引用>

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)(断言 (> a 0))(断言 (< a 1))(断言(> x 0))(断言 (< x 1))(断言(> y 0))(断言 (< y 1))(断言(> z 0))(断言 (< z 1))(断言 (> m 0))(断言 (< m 1))(断言(= (* (* a a) a) m))(断言(=(*(* x y)z)m))(断言 (> (* 3.0 a) (+ (+ z y) x) ))(检查周六)

模型不满意.

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

解决方案

您的解决方案是正确的.

说明:你写的等价于:

0 <×＜10＜y＜10＜＜10＜米＜1a * a * a = mx * y * z = 米3 * a >x + y + z

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

<块引用>

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

那么不可能是这样的:

<块引用>

3a > (x+y+z)

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

I'm a total newbie with Z3 (started today). So far liking it a lot. Great tool. Unfortunately the syntax confuses me a bit.

I want to prove that if:

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

then:

3a <= (x+y+z)

I do so by trying to find a model satisfying that:

3a > (x+y+z)

Here is the Z3 code:

(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)

The model is unsatisfied.

Have I successfully proved what I wanted? As I said, the syntax confuses me since I'm a total newbie.

解决方案

Your solution is correct.

Explanation: What you wrote is equivalent to:

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 says this is unsatisfiable. Thus, if

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

then it cannot be the case that:

3a > (x+y+z)

because, if this did occur, then the SMT problem you posed would be satisfiable, which would be a contradiction with the claim by Z3 that the SMT problem is unsatisfiable. If it cannot be the case that 3a > (x+y+z), then it must be the case that 3a <= (x+y+z), which is the statement you originally wanted to prove.

这篇关于Z3 表明如果 a^3=x*y*z 那么 3a <= x+y+z的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！