策略求解器超時的錯誤行爲

Question

我試圖在Z3中使用策略求解器來解決與通用求解器相反的一些X約束問題。

我使用以下策略 -

simplify purify-arith elim-term-ite reduce-args propagate-values solve-eqs symmetry-reduce smt sat sat-preprocess 

我申請的戰術一個又一個問題通過使用Z3_tactic_and_then API。 此外，我使用this technique爲了配置解算器的超時。

現在，對於同樣的問題，如果我使用常規解算器，它會超時查詢指定的超時時間。但是，如果我使用提到的解算器的策略，那麼它在給定的時間內不會超時。它運行時間更長。

例如，我指定了一個超時時間180*1000 milliseconds，但超時時間爲730900毫秒。 我試圖刪除上面提到的一些策略，但行爲仍然是一樣的。

Z3 4.1版

Answer 1

不幸的是，並非每一個戰術尊重超時。策略smt是一個很大的「罪犯」。這種策略包含了Z3中實現的一個非常古老的解算器。不幸的是，這個解算器在一些昂貴的計算過程中不能被中斷，因爲它會使系統處於損壞狀態。也就是說，Z3會在未來的運營中崩潰。當這個求解器被實現時，使用了一個非常簡單的設計。如果我們要中斷進程：殺了它。當然，當在更大的應用中使用Z3時，這是不可接受的。新代碼通常對超時更敏感，我們試圖避免這種糟糕的設計。