z3在非線性約束下超時

Question

當使用z3進行非線性實數運算時，我有一個超時問題。下面的代碼是檢查4維超矩形是否具有大於50000的體積並且還滿足一些約束。但z3在1分鐘內無法給出答案。如何讓它更快？

a0min = Real('a0min') 
a0max = Real('a0max') 
a1min = Real('a1min') 
a1max = Real('a1max') 
a2min = Real('a2min') 
a2max = Real('a2max') 
a3min = Real('a3min') 
a3max = Real('a3max') 
volume = Real('volume') 

s = Tactic('qfnra-nlsat').solver() 

s.add(-a0min * (1.0 - a1max) + a2max * a3max <= -95000.0, 
a0min > 0.0, 
a0min < a0max, 
a0max < 1000000.0, 
a1min > 0.0, 
a1min < a1max, 
a1max < 1.0, 
a2min > 1.0, 
a2min < a2max, 
a2max < 1000.0, 
a3min > 1.0, 
a3min < a3max, 
a3max < 50.0, 
(a0max - a0min) * (a1max - a1min) * (a2max - a2min) * (a3max - a3min) > 50000.0, 
volume == (a0max - a0min) * (a1max - a1min) * (a2max - a2min) * (a3max - a3min)) 
print s.check() 

而且還有一件有趣的事：如果與更換一些「>」和「<」「< =」和「> =」，Z3的求解器可以在兩秒鐘返回答案。相應的代碼如下。任何人都知道這是爲什麼發生？

a0min = Real('a0min') 
a0max = Real('a0max') 
a1min = Real('a1min') 
a1max = Real('a1max') 
a2min = Real('a2min') 
a2max = Real('a2max') 
a3min = Real('a3min') 
a3max = Real('a3max') 
volume = Real('volume') 

s = Tactic('qfnra-nlsat').solver() 

s.add(-a0min * (1.0 - a1max) + a2max * a3max <= -95000.0, 
a0min >= 0.0, 
a0min <= a0max, 
a0max <= 1000000.0, 
a1min >= 0.0, 
a1min <= a1max, 
a1max <= 1.0, 
a2min >= 1.0, 
a2min <= a2max, 
a2max <= 1000.0, 
a3min >= 1.0, 
a3min <= a3max, 
a3max <= 50.0, 

(a0max - a0min) * (a1max - a1min) * (a2max - a2min) * (a3max - a3min) > 50000.0, 
volume == (a0max - a0min) * (a1max - a1min) * (a2max - a2min) * (a3max - a3min)) 
print s.check() 

Answer 1

在第一種情況下，Z3用真代數數字「卡住」計算。如果我們幾分鐘後

valgrind --tool=callgrind python nl.py 

中斷執行腳本，並運行

kcachegrind 

我們將看到，Z3被卡內algebraic_numbers::isolate_roots。 nlsat求解器使用的當前實數代數包非常低效。 我們有一個用代數數字計算的new package，但它還沒有與nlsat集成。

避免代數數字計算的一個訣竅是隻使用嚴格的不等式。等於volume == ...是無害的，因爲它在預處理時間被消除。 如果我們用-a0min * (1.0 - a1max) + a2max * a3max < -95000.0代替第一個約束，那麼Z3也會很快終止（也可以在線獲得here）。

a0min = Real('a0min') 
a0max = Real('a0max') 
a1min = Real('a1min') 
a1max = Real('a1max') 
a2min = Real('a2min') 
a2max = Real('a2max') 
a3min = Real('a3min') 
a3max = Real('a3max') 
volume = Real('volume') 

s = Tactic('qfnra-nlsat').solver() 

s.add(-a0min * (1.0 - a1max) + a2max * a3max < -95000.0, 
a0min > 0.0, 
a0min < a0max, 
a0max < 1000000.0, 
a1min > 0.0, 
a1min < a1max, 
a1max < 1.0, 
a2min > 1.0, 
a2min < a2max, 
a2max < 1000.0, 
a3min > 1.0, 
a3min < a3max, 
a3max < 50.0, 
(a0max - a0min) * (a1max - a1min) * (a2max - a2min) * (a3max - a3min) > 50000.0, 
volume == (a0max - a0min) * (a1max - a1min) * (a2max - a2min) * (a3max - a3min)) 
print s.check() 
print s.model() 

順便說一句，當你與<=取代一切，nlsat仍然有使用真正的代數計算，但變化影響nlsat搜索樹，並設法找到解決它陷在一個真正的代數前數量計算。

這裏有三個地方nlsat在我們試圖實例被「卡住」 /審查

• 實代數數計算（如你的例子）。當我們用新的包替換當前的包時，這將被修復。

• 多項式因式分解。 Z3中實現的當前算法效率非常低。這也可以修復。

• Subresultant computations。這一點很棘手，因爲據我所知Z3使用了非常有效的實現。性能與Mathematica等先進系統的實現類似。當Z3回溯搜索時使用此操作。好的屬性是我們可以證明Z3總是會使用這種方法終止。另一種選擇是考慮不保證終止但更便宜的近似方法。不幸的是，這不是像前兩個那樣的小改變。