控制Z3的解決策略

Question

所以我們假設我有一個很大的問題需要在Z3中解決，如果我試圖在一個解決方案中解決它，它會花費太多的時間。所以我把這個問題分成幾部分並分別解決。 作爲一個玩具的例子，假設我複雜的問題是要解決那些3個方程：

eq1: x>5 
eq2: y<6 
eq3: x+y = 10 

所以我的問題是，是否例如將有可能首先要解決EQ1和EQ2。然後使用結果解決eq3。

assert eq1 
assert eq2 

(check-sat) 

assert eq3 
(check-sat) 
(get-model) 

似乎工作，但我不知道它是否有意義performancewise？ 增量求解可能會幫助我嗎？或者，我還可以使用z3的其他功能來分割我的問題嗎？

Answer 1

所考慮的問題通常是可滿足性問題，即目標是找到一個一個解決方案（模型）。滿足的解決方案（模型）不一定滿足eq3，因此您不能將問題減半。我們必須爲找到全部解決方案（型號），以便我們可以用該（一組）解決方案替換xeq3。 （例如，這是矩陣對角線後的高斯消元中發生的情況。）