Z3 极性使用 Z3 作为 SAT 求解器 [英] Z3 Polarity using Z3 as SAT Solver

问题描述

我正在尝试使用 Z3 解决 12000 多个布尔变量的 SAT 问题.我希望大多数变量在解决方案中评估为假.有没有办法引导或提示 Z3 作为 SAT 求解器首先尝试极性错误"?我已经尝试过使用 cryptominisat 2 并取得了不错的结果.

I am trying to solve a SAT problem with 12000+ boolean variables using Z3. I expect that most of the variables will evaluate to false in the solution. Is there a way to guide or hint Z3 as SAT solver to try "polarity false" first? I've tried it with cryptominisat 2 and got good results.

推荐答案

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

Z3 is a collection of solvers and preprocessors. We can provide hints for some of the solvers. When the command (check-sat) is used, Z3 will select the solver automatically for us. We should (check-sat-using <strategy>) if we want to select the solver ourselves. For example, the following command will instruct Z3 to use a Boolean SAT solver.

(check-sat-using sat)

我们可以强制它总是先尝试polarity false":

We can force it to always try "polarity false" first by using:

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

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

We can also control the preprocessing steps. If we want to put the formula in CNF before invoking sat, we should use:

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

EDIT:如果您使用 DIMACS 输入格式和 Z3 v4.3.1，则无法使用命令行为所有可用求解器设置参数.下一个版本将解决这个限制.同时，您可以使用以下命令下载 work-in-progress 分支:

EDIT: if you are using the DIMACS input format and Z3 v4.3.1, then you can't set parameters for all available solvers using the command line. The next release will address this limitation. In the meantime, you can download the work-in-progress branch using:

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

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

and compile Z3. Then, to force polarity false, we use the command line option

sat.phase=always_false

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

The command z3 -pm:sat will display all available options for this module.

结束编辑

以下是 SMT 2.0 中的完整示例(也可在线):

Here is a complete example in SMT 2.0 (also available 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)

这篇关于Z3 极性使用 Z3 作为 SAT 求解器的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！