由于这个问题有点难以描述，我将用一个小例子来描述我的问题。假设有一个命题公式集，其元素是布尔变量 a、b 和 c。当使用 z3 得到这个公式集的真值赋值时，是否存在一些方法来设置变量的优先级？我的意思是如果优先级是a>b>c，那么在搜索过程中z3首先假设a为真，如果a不可能为真，则假设b为真，依此类推。换句话说，如果 z3 给出了一个真值赋值：not a,b,c 在上述优先级下，这意味着 a 不可能为真，因为 a 与 b 相比具有高优先级。希望我清楚地描述这个问题。
问问题
348 次
1 回答
4
在当前版本（v4.3.1）中没有简单的方法来做到这一点。我能看到的唯一方法是破解/修改 Z3 源代码 ( http://z3.codeplex.com )。我们同意设置优先级对于某些应用程序是一个有用的功能，但是也存在一些问题。
首先，Z3 在解决问题之前应用了几个转换（也称为预处理步骤）。创建和消除变量。因此，对于由 Z3 解决的实际问题（应用所有变换后生成的问题），原始问题的案例分割优先级可能没有意义。
一个戏剧性的例子是一个只包含位向量的公式。默认情况下，Z3 会将此公式简化为命题逻辑并调用命题 SAT 求解器。在这种减少中，所有的位向量变量都被消除了。
Z3 是求解器和预处理器的集合。默认情况下，Z3 会自动为用户选择求解器。其中一些求解器使用完全不同的算法。因此，提供的优先级可能对正在使用的求解器无用。
正如GManNickG 所指出的，可以为特定求解器设置相位选择策略。有关更多详细信息，请参阅他评论中提供的帖子。
于 2013-01-13T16:03:55.663 回答