z3 - 我可以在 z3 中设置 bool 变量的优先级吗？

Question

由于这个问题有点难以描述，我将用一个小例子来描述我的问题。
假设有一个命题公式集，其元素为 bool 变量 a、b 和 c。
当使用 z3 获得此公式集的真值分配时，是否存在某种方法来设置变量的优先级？我的意思是，如果优先级是 a>b>c，那么在搜索过程中 z3 首先假定 a 为真，如果 a 不可能为真，则假定 b 为真，依此类推。换句话说，如果 z3 给出了一个真值分配:在上述优先级下不是 a,b,c，则意味着 a 不可能为真，因为与 b 相比，a 是高优先级。希望我清楚地描述了这个问题。

Answer 1

在当前版本 (v4.3.1) 中没有简单的方法来做到这一点。我能看到的唯一方法是破解/修改 Z3 源代码 ( http://z3.codeplex.com )。我们同意设置优先级对于某些应用程序是有用的功能，但是存在一些问题。

首先，Z3 在解决问题之前应用多个转换(也称为预处理步骤)。变量被创建和消除。因此，原始问题的 case-split 优先级对于由 Z3 解决的实际问题(应用所有转换后生成的问题)可能没有意义。

一个戏剧性的例子是一个仅包含位向量的公式。默认情况下，Z3 会将此公式简化为命题逻辑并调用命题 SAT 求解器。在这种减少中，消除了所有位向量变量。

Z3 是求解器和预处理器的集合。默认情况下，Z3 会自动为用户选择求解器。其中一些求解器使用完全不同的算法。因此，提供的优先级可能对正在使用的求解器无用。

如 GManNickG指出，可以为特定求解器设置相位选择策略。有关更多详细信息，请参阅他的评论中提供的帖子。