Z3是否會在求解線性實數算術約束時自適應地改變策略？

Question

我有一套巨大的線性實數算術約束來解決，我逐漸將它們餵給解算器。一段時間後Z3似乎總是卡住。 Z3內部是否會改變其解決約束的策略，例如從Simplex算法轉移到另一個等等，還是我必須明確指示Z3這樣做？我正在使用Z3py。

Answer 1

沒有進一步的細節，不可能精確地回答這個問題。

通常，如果沒有設置邏輯並運行默認策略或調用(check-sat)而沒有其他選項，Z3將在第一次看到push命令時切換到另一個求解器;在此之前它可以使用非增量求解器。

增量求解器帶有增量求解器的所有正面和負面，也就是說，它最初可能會更快，但它可能無法在一段時間後利用以前學習的引理，並且它可能只記得太多不相關的事實。此外，啓發式可能會「記住」以後不適用的信息，例如，在所有內容被彈出之後，「好」變量排序可能會變成錯誤的排序，並推出相同變量的不同問題。過去，一些用戶發現它對於一些查詢使用增量求解器更好，但是當它變得太慢時從頭開始。