z3py：什麼是斷言「東西不存在」約束的正確方法

Question

我想在z3py中聲明「東西不能存在」的約束。我嘗試使用「Not（Exists（...））」。一個簡單的例子如下。我想爲a和b找到一個賦值，以便這樣的c不存在。

from z3 import * 

s = Solver() 
a = Int('a') 
b = Int('b') 
c = Int('c') 

s.add(a+b==5) 
s.add(Not(Exists(c,And(c>0,c<5,a*b+c==10)))) 
print s.check() 
print s.model() 

輸出是

sat 
[b = 5, a = 0] 

這似乎是正確的。 但是，當我在更復雜的問題中編寫「Not（Exists（...））」約束時，需要幾個小時而不生成解決方案。 我不知道這是否是正確和最有效的方式來斷言「不存在」約束？或者量子的這些問題本質上很難由任何求解器來解決？

Answer 1

你寫這個約束的方式很好。 Z3（或任何其他解算器）將很難解決諸如量詞和非線性算術等問題，這並不奇怪。這些問題本質上很難解決。

你可能會考慮Z3的nlsat戰術，這可能會帶來一些緩解：How does Z3 handle non-linear integer arithmetic?

或者，你可以嘗試real！而非整數或位向量（即機器整數）。當然，您是否可以真正使用這些類型取決於您的問題域。 （Reals顯然會有「小數」值，並且位向量需要進行模運算。）