證明是n^5 <= 5^N對於n> = 5

Question

使用以下代碼：

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和之間的界面楓。 Clemens Ballarin。卡斯滕霍曼。雅克·卡爾梅特。使用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更直接的證據。非常感謝。

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