如何让 z3 生成不可满足的证明？答案

【问题标题】：How to make z3 generate proof of unsatisfiability?如何让 z3 生成不可满足的证明？
【发布时间】：2019-12-21 23:19:50
【问题描述】：

我正在尝试使用 命令行 中的 z3 作为 SAT 求解器，但我不知道如何使它生成不可满足的证明。无论我做什么，它只会打印“unsat”而没有任何解释，而且我在网上找不到任何帮助。我尝试在命令行上传递proof=true，但没有任何改变。

../z3-4.8.6-x64-ubuntu-16.04/bin/z3 proof=true unsat_core=true test_tx.cnf 
unsat

【问题讨论】：

标签： z3 sat

【解决方案1】：

z3 可以在 SMTLib 模式下生成证明（尽管证明格式相当不确定。）我不确定它是否甚至可以在 CNF 模式下生成证明，尽管它肯定是可能的。您最好的选择可能是在 https://github.com/Z3Prover/z3/issues 提交问题，看看是否支持。

【讨论】：