在线使用Z3Py证明n^5 <= 5 ^n for n >= 5答案

【问题标题】：Using Z3Py online to prove that n^5 <= 5 ^n for n >= 5在线使用Z3Py证明n^5 <= 5 ^n for n >= 5
【发布时间】：2013-04-28 23:27:32
【问题描述】：

使用以下代码：

n = Int('n')
s = Solver()
s.add(n >= 5)
s.add(Not( n**5 <= 5**n))
print s
print s.check()

我们得到以下输出：

[n ≥ 5, ¬(n^5 ≤ 5^n)]
unknown

也就是说Z3Py不能直接证明。

现在使用代码

n = Int('n')
prove(Implies(n >= 5, n**5 <= 5**n))

Z3Py 也失败了。

一个可能的间接证明如下：

n = Int('n')
e, f = Ints('e f')
t = simplify(-(5 + f + 1)**5 + ((5 + f)**5 + e)*5, som=True)
prove(Implies(And(e >=0, f >= 0), t >= 0))

输出是：

proved

使用 Isabelle + Maple 的证明见：定理和算法：Isabelle 和 Maple 之间的接口。克莱门斯·巴拉林。卡斯滕霍曼。雅克·卡尔梅特。

其他可能使用 Z3Py 的间接证明如下：

n = Int('n')
e, f = Ints('e f')
t = simplify(-(5 + f + 1)**5 + ((5 + f)**5 + e)*5, som=True)
s = Solver()
s.add(e >= 0, f >= 0)
s.add(Not(t >= 0))
print s
print s.check()

输出是：

[e ≥ 0,
f ≥ 0,
¬(7849 +
9145·f +
4090·f·f +
890·f·f·f +
95·f·f·f·f +
4·f·f·f·f·f +
5·e ≥
0)]
unsat

如果可以使用 Z3Py 进行更直接的证明，请告诉我。非常感谢。

【问题讨论】：

Z3 没有整数算术的决策程序，也没有权力。您对简化的使用在我看来非常巧妙，可以结合可用的功能。

标签： z3

【解决方案1】：

Z3 对非线性整数运算的支持非常有限。有关详细信息，请参阅以下相关帖子：

How does Z3 handle non-linear integer arithmetic?

Z3 有一个完整的求解器 (nlsat) 用于非线性实数（多项式）算术。你可以通过编写来简化你的脚本

n = Real('n')
e, f = Reals('e f')
prove(Implies(And(e >=0, f >= 0), -(5 + f + 1)**5 + ((5 + f)**5 + e)*5 >= 0))

Z3 在上述问题中使用 nlsat，因为它只包含实变量。即使问题包含整数变量，我们也可以强制 Z3 使用 nlsat。

n = Int('n')
e, f = Ints('e f')
s = Tactic('qfnra-nlsat').solver()
s.add(e >= 0, f >= 0)
s.add(Not(-(5 + f + 1)**5 + ((5 + f)**5 + e)*5 >= 0))
print s
print s.check()

【讨论】：