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

Question

我试图使用Z3解决12000+布尔变量的SAT问题.我希望大多数变量在解决方案中评估为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))

我们还可以控制预处理步骤.如果我们想在调用之前将公式放在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.然后,为了强制极性为false,我们使用命令行选项

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)