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

[Jochen Hoenicke]

Hello Tjark,

Thanks for your feedback.

On Tue, 20 Jul 2021 at 15:51, Tjark Weber <tjark.weber at it.uu.se> wrote:
>
> Jochen,
>
> On Mon, 2021-07-19 at 16:44 +0200, Jochen Hoenicke wrote:
> > Yesterday, I mentioned the plans for the Proof Validation Track. I
> > know that finding a good solver independent proof format is
> > difficult.
>
> Indeed it is. Nearly ten years ago, Sascha Böhme and I -- having worked
> extensively with existing proof formats at the time -- discussed some
> high-level considerations that I think are still relevant today: see
> http://user.it.uu.se/~tjawe125/publications/boehme11designing.pdf
>
> > I would like to go with something simple with a minimal but complete
> > set of axioms.  Then every solver has the same burden to translate
> > its own proof steps into this simple format.
>
> There are trade-offs: a simple proof format makes it easier to
> implement a proof checker but makes it more difficult/laborious to
> generate proofs, and might also lead to larger proofs.
>
> > I would be interested in some feedback.  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.
>
> My initial impression (not based on any experimental data) is that your
> proposal isn't necessarily hitting the sweet spot in the available
> design space. I understand that you want the proof checker to be
> simple, but for instance differentiating between (or a b) and (or b a)
> could be a pain in solvers (and lead to considerable proof overhead),
> while it would probably be relatively easy in the checker to treat a
> disjunction as a set of disjuncts (as long as there is no ambiguity).

The problem here is where to draw a line, if you want commutative or,
you probably also want associative or, the same for and, xor, +, *,
bvmul, bvadd.  Then maybe commutativity for fpmul and fpadd, which
aren't associative.  Then you naturally also want to rewrite - to +
and negation so that associativity can also be used for that. Finally
you end up with an almost intractable problem for the proof checker to
determine what formula was proven.  I don't want the resolution rule
to care about which builtin operator is associative or commutative,
especially when a full proof may take millions of resolution steps.
I'd rather put the burden on the solver author's who know what
simplification steps their solver may do and when the solver does
them.  I don't want to write a universal simplifier that works for
most of the solvers and needs to be extended whenever a new solver
enters the field.

But after some discussions with Pascal, Clark, and Bruno it looks like
it would not be feasible for most solvers to produce fully verifiable
low-level proofs, especially when they use advanced techniques like
symmetry breaking.  As a compromise, we could allow the solver to
assert arbitrary clauses where they just give a hint from which input
these clauses were generated and some solver-specific information,
that helps their own proof-checker to understand the proof.  These
solver specific rules would be skipped by the proof-checker and it
could also produce a proof obligation in the form of an SMT-file to
check that the asserted clauses are indeed a consequence.  Thus, if a
solver does some commutativity rewrite, it could just assert the
converted formula and state that it's a consequence of the input
formula.  The end-goal would be to get rid of these trusted steps,
e.g., by a postprocessor, but this end-goal may take years to achieve.

Another raised concern is that some solvers want to introduce
auxiliary variables for which they don't know an equivalent SMT term
for.  An auxiliary variable can always be introduced by "let", but
this requires knowing an equivalent SMT-LIB term.  A solver that just
dumps it's internal converted CNF using the unchecked rule, may want
to use new uninterpreted symbols and only claim equisatisfiability of
the CNF with the original formula.  I'm thinking about a kind of
"exists"-binder for the whole proof to create new uninterpreted
auxiliary variables.

A proof validation competition may be a very high goal for next year.
If you allow unexplained steps in your proof you cannot compare the
proofs of two solvers.  One solver may use hundreds of unexplained
steps that just do a small rewrite that is easy to see while the other
solver may use a single unexplained step that derives false from the
input formula.  In most metrics the second solver would win, even
though the first does a much better job.  Maybe we can have a proof
exhibition, but this time with a fixed syntax so that an independent
proof checker can track the resolution steps of the proof and document
how many untrusted steps were needed and which.  We could also
preprocess some benchmarks into a simple CNF form and run the solvers
on the simplified benchmark, so that no major pre-processing has to be
done.

Lastly, the common proof format doesn't have to become the default
proof format of every solver.  If you like your proof format, then by
all means you can keep it.  Just write a post-processor that
translates the easy steps into low-level proof steps and skips the
hard steps in your proof.

>
> My understanding is that the SAT community is using DRAT for good
> reasons (including performance). Given that SMT is an extension of SAT,
> and that SMT solvers often use a SAT solver internally, I think it
> might be worth looking into DRAT in more detail, and investigate if it
> wouldn't be beneficial to base a proof format for SMT on (a suitable
> extension of) DRAT. An easy test for any SMT proof format is how it
> performs on (large) purely propositional problems.

I definitely will look into DRAT and plan to write a translator for
these proofs at least to test the overhead this induces.  The problem
with including the unmodified RAT rule is that it changes the meaning
of an atom.  This is possible in the SAT context, where you know every
clause containing the atom and where an atom is uninterpreted. I don't
see how to do this in an SMT proof, especially when an atom is an SMT
term and you always want to be able to introduce arbitrary theory
lemmas for every literal in your proof.  But it is possible to use
extended resolution to compactly represent a DRAT proof.  There one
would explicitly redefine the meaning of literals and reproof the
known facts for the redefined literal.

  Jochen