Streaming LRAT Certificates into Lean Theorems

Abstract

If the certificate produced by a SAT solver is checked by a verified checker, we get a verdict which convinces. But this verdict cannot be named, reused as a lemma, or composed with other formal developments. We propose the tool lrat-catcher, which turns a certificate into a Lean theorem. It checks the certificate as a stream while the solver is still running. Hence the certificate is not required to be saved to a file. Additionally, our tool makes Lean core's verified LRAT checker resumable so that its state can be serialized. We prove that checking divided at such a state still properly refutes the original formula. We propose two import modes. The stream mode reads the certificate from a pipe in blocks and checks it on the fly in memory. The file mode imports a stored certificate in chunks. If interrupted, it rechecks only the chunks it has not yet completed. The soundness theorem for the stream mode guarantees that a garbled or adversarial stream can only fail the check but not yield a false theorem. We find that with compaction at chunk boundaries, the memory required depends only on the live clause set, not on the certificate size. Our tool supports cube-and-conquer and formulas derived by preprocessing, to still form Lean proofs of the original formula. We provide several end-to-end case studies on well-known combinatorial problems. A larger scaling experiment on the empty-hexagon problem shows that 174 TB of certificates can be imported into Lean via streaming.

Abstract: arXiv descriptive metadata (CC0). Thank you to arXiv for use of its open access interoperability. This service was not reviewed or approved by, nor does it necessarily express or reflect the policies or opinions of, arXiv.