On proof generation and proof checking

[rainoftime]

Many applications require a verifier for SMT refutations. That is, the solver accompanies its unsat answers with a certificate that can be checked independently with much simpler and more trustworthy tools (i.e., a proof checker). This certificate is, in general, proof of the input formula’s unsatisfiability, expressed as a proof term in some suitable proof system (such as propositional resolution).

• For purely SAT problems, there is a commonly used standard DRAT (also supported by z3). E..g, https://www.cs.utexas.edu/~marijn/drat-trim/
• For SMT problems, different SMT solvers (e.g., CVC4, Z3, SMTInterpol) have different formats for proof, and they may have some internal tools for proof checking. A major challenge is to devise a common proof system. The wide diversity of theories and solving algorithms in SMT makes it difficult to find a single proof system that is universally good.

---

Related discussions about Z3

• Question: Proof Checking in Z3 - state of the art #5000
• Refutation verification #4226

---

Some papers for reference

• Proof Reconstruction for Z3 in Isabelle/HOL https://www21.in.tum.de/~boehmes/proofrec.pdf
• Towards bit-width-independent proofs in SMT solvers. CADE'19
• DRAT-based bit-vector proofs in CVC4, SAT'19
• Lazy proofs for DPLL(T)-based SMT solvers. FMCAD'16
• Fine-grained SMT proofs for the theory of fixed-width bit-vectors. LPAR'15
• SMT proof checking using a logical framework, FMSD'13
• Fast and flexible proof checking for SMT, SMT'09

---

A successful story of proof generation in SAT
Marijn Heule used a parallel SAT solver to prove the Boolean Pythagorean Triples problem, which dumps a proof of 200 TB in size

Nature Volume 543: 17-18: Maths proof smashes size record [http://www.nature.com/news/two-hundred-terabyte-maths-proof-is-largest-ever-1.19990]
(Reddit offers a discussion on this article with 250+ comments https://www.reddit.com/r/science/comments/4lnpm8/twohundredterabyte_maths_proof_is_largest_ever/)

[NikolajBjorner]

NB update: the drat format mentioned in this comment is now deprecated for SMT queries.
You can still get DRAT (DRUP) proofs from DIMACS inputs (file extension .cnf or .dimacs). SMT proofs use (a mild extension of) SMTLIB syntax so they can be processed using SMTLIB parsers.

The main development in Z3 regarding proofs is to support an SMT extension of DRUP (DRAT). I am using it to debug a new core. While the new core is not ready for prime time developing the proof logging format and checker is integral for the development.
The format syntax is summarized in

https://github.com/Z3Prover/z3/blob/master/src/sat/sat_drat.h

It is currently producing theory lemmas for arithmetic, cardinality and PB constraints, bit-vectors, arrays, and EUF.

There is a domestic checker invoked from the command line by using two files:

    z3.exe <original-input>.smt2 log.drat

where log.drat is obtained

   z3.exe <original-input>.smt2 sat.euf=true tactic.default_tactic=sat sat.drat.file=log.drat

While I can't take bug reports yet for runs using sat.euf small examples may be able to give an idea of its usage.
The domestic checker is crude: one part of it does not handle recycling of propositional variables (if deleting all clauses that contain a Boolean variable it may be used for a different atomic formula), the other part that can handle it relies on a full SMT check and does not benefit from efficient unit propagation as a good forward DRUP checker would.
So there is a good opportunity to create a self-contained proof checker for DRUP(T).
I am currently using the crude self-checker to isolate a known bug (but not known root cause) around recycling Boolean variables for bit-vector theories.

[andrewjlawrence]

Hi @NikolajBjorner, has any progress been made on this issue? I am interested in using such a proof checker with Z3 and may develop one but obviously there is no point in that if someone else has developed such a proof checker already.

[NikolajBjorner]

Here is a set of slides with an introduction to ongoing efforts
https://z3prover.github.io/slides/proofs.html#/

[andrewjlawrence]

Will this seminar be recorded and made available online?

[NikolajBjorner]

It is a draft for a Dagstuhl seminar talk in about 2 weeks from now.
I don't think they record talk. Dagstuhl is geared towards a semi-informal in-person setting.

The slides are being prepared so they can also be a reference point for the people in SAT community that work on proof logging for variants of SAT solvers (PB solvers, CP, BDDs) to get an idea of what applies in the SMT space.

To prepare for this talk I am also filling in more gaps in the proof tools for the new core. I added EUF format and checking last weekend and plan to carve out trimming.

There is a ton of work in testing and filling in details. For covering SMT theories, it is essentially open ended (I think the related work citations give a good idea of how many incremental papers got cranked out on this topic alone). To scale this effort it is useful to involve contributions. Contributers can get acquainted with internals by adding proof extractions for selected theories (bit-vectors or ADTs) that were previously studied (or I add such axioms in down-time and based on needs), or transforming coarse-grained proofs into formats understood by SMTInterpol (the slides mention how Farkas axioms are coarser grained when produced by z3 than from SMTInterpol, but they are essentially the same).