使用Z3作为Z3求解器的SAT极性

Question

我正在尝试用Z3解决一个带有12000+布尔变量的应用程序测试问题。我期望大多数变量在解决方案中的计算结果为false。有没有一种方法可以引导或提示Z3作为SAT求解器首先尝试“极性错误”？我已经用cryptominisat 2试过了，效果很好。

Answer 1

Z3是求解器和预处理器的集合。我们可以为一些求解器提供提示。当使用(check-sat)命令时，Z3会自动为我们选择求解器。如果我们想自己选择求解器，我们应该使用(check-sat-using <strategy>)。例如，以下命令将指示Z3使用布尔SAT求解器。

(check-sat-using sat)

我们可以强制它总是先尝试“极性假”，方法是：

(check-sat-using (with sat :phase always-false))

我们还可以控制预处理步骤。如果我们想在调用sat之前将公式放在CNF中，我们应该使用：

(check-sat-using (then tseitin-cnf (with sat :phase always-false)))

编辑解算器:如果您使用的是DIMACS输入格式和Z3 v4.3.1，那么您不能使用命令行为所有可用的求解器设置参数。下一版本将解决此限制。同时，您可以使用以下命令下载正在进行中的分支：

git clone https://git01.codeplex.com/z3 -b unstable 

并编译Z3。然后，为了强制极性为false，我们使用命令行选项

sat.phase=always_false

命令z3 -pm:sat将显示此模块的所有可用选项。

结束编辑

下面是一个完整的SMT2.0示例(也可以使用online)：

(declare-const p Bool)
(declare-const q Bool)
(declare-const r Bool)
(declare-const s Bool)

(assert (or (not p) (not q) (not r)))
(assert (or r s))
(assert (or r (not s)))
(assert (or r (and p q)))

(echo "With always false")
(check-sat-using (then tseitin-cnf (with sat :phase always-false)))
(get-model)
(echo "With always true")
(check-sat-using (then tseitin-cnf (with sat :phase always-true)))
(get-model)