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

Question

我正在尝试使用 Z3 解决具有 12000 多个 bool 变量的 SAT 问题。
我希望大多数变量在解决方案中都会评估为假。
有没有办法引导或提示 Z3 作为 SAT 求解器首先尝试“极性错误”？
我已经用 cryptominisat 2 试过了，结果很好。

Answer 1

Z3 是求解器和预处理器的集合。我们可以为一些求解器提供提示。
当命令(check-sat)使用时，Z3 会自动为我们选择求解器。
我们应该 (check-sat-using <strategy>)如果我们想自己选择求解器。
例如，以下命令将指示 Z3 使用 bool 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。然后，为了强制极性为假，我们使用命令行选项

sat.phase=always_false

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

结束编辑

这是 SMT 2.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)