z3 - 我可以在 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) asks the solver for a proof of unsatisfiability for the set of all formulas in the current context. The command can be issued only if the most recent check command had an empty set of assumptions. The solver responds by printing a refutation proof on its regular output channel. The format of the proof is solver-specific. The only requirement is that, like all responses, it be a member of s_expr.

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

在定理证明器中回放

Isabelle theorem prover可以回读Z3的证明并在内部重放以构造相应的证明。这可能更接近您要查找的内容。这是描述这项工作的论文:http://www21.in.tum.de/~boehmes/proofrec.pdf当然，具体支持哪些逻辑和是否主动维护连接是另外一个问题!您可能会发现该论文的“相关工作”部分很有帮助。