我可以在 Z3 中重放证明吗？

Question

是否可以让 Z3 序列化某个断言的证明，并在以后的调用中重放证明而不是再次运行证明搜索？我知道 Z3 可以输出 的反例unsat，但它可以为 的模型提供证明sat吗？

Answer 1

术语说明：Z3（以及一般的 SAT/SMT 求解器）输出模型sat，以及证明unsat。

证明生成实际上是一个 SMT-Lib 功能。参见http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2017-07-18.pdf 的第 56 页

而且Z3确实支持它，这是最简单的例子：

(set-option :produce-proofs true)
(declare-fun a () Bool)
(assert (= a (not a)))
(check-sat)
(get-proof)

Z3 说：

unsat
((proof
(mp (asserted (= a (not a))) (rewrite (= (= a (not a)) false)) false)))

格式是特定于求解器的。SMTLib 文档说：

(get-proof) 要求求解器提供当前上下文中所有公式集的不可满足性证明。仅当最近的检查命令具有空假设集时才能发出该命令。求解器通过在其常规输出通道上打印反驳证明来做出响应。证明的格式是特定于求解器的。唯一的要求是，像所有响应一样，它是 s_expr 的成员。

据我所知，没有“公开”开关告诉 Z3 读回这个证明并用它做任何事情。然而，他们可能拥有使用此输出的内部工具，这并不令我感到惊讶。

在定理证明器中重放

Isabelle 定理证明器可以读回 Z3 的证明并在内部重放它们以构建相应的证明。这可能更接近您正在寻找的内容。这是一篇描述这项工作的论文：http: //www21.in.tum.de/~boehmes/proofrec.pdf 当然，究竟支持哪些逻辑以及是否主动维护连接是另一个问题！您可能会发现该论文的“相关工作”部分非常有帮助。