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

Question

我正在尝试使用 Z3 解决具有 12000 多个布尔变量的 SAT 问题。我希望大多数变量在解决方案中都会评估为假。有没有办法引导或提示 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))

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

(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 中的完整示例（也可在线获取）：

(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)