我可以在z3中設置布爾變量的優先級嗎？

Question

由於這個問題有點難以描述，我將用一個小例子來描述我的問題。 假設有一個命題公式集，其元素是布爾變量a，b和c。 當使用z3獲得這個公式集的真值分配時，是否存在某種方法來設置變量的優先級？我的意思是，如果優先級是> b> c，那麼在搜索過程中，z3首先假設a爲真，如果a不可能爲真，則假設b爲真，依此類推。換句話說，如果z3給出了真值賦值：在上述優先級下不是a，b，c，這意味着a不可能是真的，因爲a與b相比是高優先級的。希望我清楚地描述這個問題。

Answer 1

在當前版本（v4.3.1）中沒有簡單的方法。我能看到的唯一方法是破解/修改Z3源代碼（http://z3.codeplex.com）。我們同意設置優先級對於某些應用程序是一個有用的功能，但是有一些問題。

首先，Z3在解決問題之前應用幾個變換（即預處理步驟）。變量被創建並消除。因此，原始問題的案例分解優先級對於由Z3解決的實際問題（應用所有變換後生成的問題）可能沒有意義。

一個戲劇性的例子是一個只包含比特向量的公式。默認情況下，Z3會將此公式減少爲命題邏輯並調用命題SAT求解器。在這種減少中，全部位矢量變量被消除。

Z3是求解器和預處理器的集合。默認情況下，Z3會自動爲用戶選擇一個求解器。其中一些解算器使用完全不同的算法。因此，所提供的優先級對於正在使用的求解器可能沒有用處。

由於GManNickG指出，可以爲特定求解器設置相位選擇策略。查看他評論中提供的帖子以獲取更多詳細信息。