以增量方式使用z3但會導致更多時間

Question

我正嘗試使用Z3通過推式方法解決一個增量約束的問題，例如（< Z 100），然後（< Z 90），然後（< Z 80）。然而，當我在增量方法中使用Z3時，如果我們直接檢查（< Z 80）（快於檢查時間（< Z 80）），在增量方法中兩次增量檢查後，我發現有時會花費更少的時間以上）。

• 你能告訴我原因嗎？
• 是否因爲學習的子句太多而使搜索變慢？
• 有沒有什麼策略可以幫助我解決這個問題？

Answer 1

你很幸運，這次

你與（< Z^80）單獨儘快解決這一次可能是因爲你的算法找到了很好的優化，當它看起來更小Z，在特殊情況下你使用它。

這可能純粹是由於您的輸入數據。爲了表明它更好地直接尋找（< Z 80） - 事實並非如此，顯然 - 您必須對許多類型的輸入數據集進行多次嘗試。