舊版本與新版本Z3

Question

我有一個可以通過舊版Z3（版本2.18）非常有效地解決的實例。它在幾秒鐘內返回SAT。 但是，當我嘗試使用當前版本的Z3（版本4.3.1）時。 10分鐘後它不會返回任何結果。

下面是關於實驗的一些細節。有人可以提供一些建議嗎？

• 有4000個布爾變量和200個智力變量

• 所有約束都命題邏輯與像一個< b

• 平臺整數之間的比較：開放的SUSE Linux 12.3@thinkpad T400s的

• Z3 v2.18是去年下載的一個linux二進制文件（我現在找不到鏈接）

• Z3 v4.3.1是下載源代碼，我使用默認設置

有在SMT文件約50,000行編譯它在我的筆記本電腦，所以我不能張貼在這裏。如果有人感興趣，我會很樂意通過電子郵件發送文件。 謝謝。

Answer 1

Z3是一個求解器組合。默認配置從版本更改。 進步永遠不會單調。也就是說，新版本可能會解決更多問題，但可能會更慢，並會在某些問題上失敗。

備註：作者已通過電子郵件將他的基準發送給Z3作者。

在「工作進行中」分支，我設法用

  (set-option :smt.auto-config false) 

Here是關於如何下載「工作正在進行」分支指令來重現Z3 2.19性能。

要獲得相同的行爲，我們也有 （檢查-SAT-採用SMT）取代 （檢查-SAT）

順便說一句，在正式發佈後，我們不得不使用

  (set-option :auto-config false) 

代替

  (set-option :smt.auto-config false)