1

使用以下代码：

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 进行更直接的证明。非常感谢。

4

1 回答 1

1

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

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()
于 2013-05-01T00:50:36.673 回答