[SMT-COMP] Proof Validation Track for SMT-COMP

[Hans-Jorg Schurr]

Hi Jochen, Hello everyone,

> Yesterday, I mentioned the plans for the Proof Validation Track. I
> know that finding a good solver independent proof format is difficult.

Thanks for taking on this certainly not easy task.

I have some thoughts about all of this, mostly informed by our work
on using SMT proofs in Isabelle and and subsequent effort of using the
Alethe format in other contexts.

I get the impression that we have some similar ideas.  The QF_UF fragment
of Alethe is very similar to what you described: Axioms and resolution.
There are some rules that have a different form that were introduced
for proofs of rewriting below quantifiers, but those are not necessary
for QF_UF (veriT uses them though)

Nevertheless, I think one should think about an upgrade path for existing
solvers.  Even seemingly innocuous changes can be difficult to implement.
For example, I spent two weeks last year trying to change veriT such
that it doesn't always consider "a = b" and "b = a" as equal -- I had
to give up in the end.

The CASC theorem proving competition has a somewhat radical approach
to this: every solver has to provide a proof, but only the general
structure is prescribed and everyone can make up their own rules.
What I hear is that over time the proofs started to be very
reasonable.

I don't think this is what SMT should do, but maybe there is something
in between.  For our implementations we thought about having variants of rules
such that a stricter solver can mark rules it uses in a stricter fashion. The
worst case of this a generic "hole" rule.  Maybe a competition could show a
percentage of holes and highlight solvers with few/no holes.

> One question is how to explain the CNF encoding.  When the proof
> format supports arbitrary SMT-LIB terms as atoms, this is simple: an
> assert is just introducing a unit clause with one atom. [..]
> A solver that doesn't use Tseitin-encoding can still explain the
> clauses in its CNF conversion using these axioms and resolution.

I think, it is also very useful to make a distinction between clauses
and disjunctions.  Otherwise it's not clear if "(or a b)" is a unit or
binary clause.  I'm not sure if this is part of your proposal.

> Finally, for a compact representation of the proof, you need to
> abbreviate common subterms. For this, I would suggest using the
> standard let syntax from SMT-LIB. A difficulty added by the let
> encoding is that terms need to be considered equal if one is the let
> expansion of the other term.

In Alethe we use the standard SMT-LIB :named annotation. This draws
a clear distinction between `let`, which is part of the logic, and
the sharing. It solves the problem you mentioned.

> Especially if you are concerned that certain features of your proofs
> cannot be represented without quadratic or even exponential overhead,
> then I would like to hear these concerns. [..]
> Some SMT-solvers use SAT solvers that create DRAT proofs.  [..] they
> can be converted to extended resolution proofs with polynomial overhead.

Just a small nitpick: the extended resolution proof generated by the
translation by Kiesl et al.[1] is cubic in the number of literals.
I think the blowup is much more reasonable in practice though.

[1] https://www.cs.cmu.edu/~mheule/publications/ijcar18.pdf

Regards,
 Hans-Jörg