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

[Tjark Weber]

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).

> Some SMT-solvers use SAT solvers that create DRAT proofs.  While
> these proofs are not easily expressible using resolution, they can be
> converted to extended resolution proofs with polynomial overhead.  My
> feeling is that I would rather keep the proof validator simple and
> let someone provide an engine that converts DRAT to extended
> resolution that DRAT-based solvers can use.

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.

Best,
Tjark









När du har kontakt med oss på Uppsala universitet med e-post så innebär det att vi behandlar dina personuppgifter. För att läsa mer om hur vi gör det kan du läsa här: http://www.uu.se/om-uu/dataskydd-personuppgifter/

E-mailing Uppsala University means that we will process your personal data. For more information on how this is performed, please read here: http://www.uu.se/en/about-uu/data-protection-policy