Z3使用极性作为Z3 SAT求解(Z3 Polarity using Z3 as SAT Solve

我试图解决一个问题，SAT用Z3 12000+布尔变量。我预计大部分的变量会评估为假的解决方案。有没有一种方法来引导或暗示Z3作为SAT求解尝试“极性假”第一？我已经与cryptominisat 2试了一下，收到了较好的效果。

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)