[SMT-COMP] [SMT-LIB] SMT-COMP 2016: Draft Rules and Timeline Available

[Clark Barrett]

Mate,

Yes, this is definitely a concern.  We had an effort some years ago to
certify some of the SMT-LIB benchmarks [1].  More recently,
we've been working on a rather ambitious proof-producing version of cvc4
and we've used it to check, for example, the QF_BV statuses.
In any case, I agree that the solution of "running two solvers" is not
sufficient in the long run.  We are using it as a place-holder until
some of these other techniques mature.

-Clark

[1] http://cs.nyu.edu/~yeting/prooftrans.pdf
[2] https://cs.nyu.edu/~barrett/pubs/HBR+15-abstract.html

On Sun, May 15, 2016 at 5:55 AM, Mate Soos <soos.mate at gmail.com> wrote:

> Hi,
>
> On 05/13/2016 02:19 PM, David R. Cok wrote:
> > The procedure in the past has been to run a set of solvers and to assign
> > a status if (a) all solvers producing a sat or unsat answer agree and
> > (b) at least two solvers produce a sat or unsat answer.
> >
> > A couple years ago, after the competition in 2014, I, Aaron Stump, and
> > Clark Barrett ran a big job with a long time out (10 hours, I think) to
> > resolve the status of any benchmarks without a status. That task took a
> > few months, with the rate of progress depending on how many nodes Aaron
> > would let the task have. We succeeded on most but not all of the
> > outstanding unknown benchmarks. It would be straightforward to do so
> > again, but it does take some time.
>
> I would like to say that it can be dangerous to do that. I remember this
> one bug [1] in gcc that made all variants of MiniSat (essentially all
> top SAT solvers except for lingeling) return the wrong answer for a
> particular set of problems [2]. I know this sounds like the stuff of
> nightmares, but it actually happened and affected all these solvers for
> years. Nowadays we have proof verification in SAT [3] so I think
> everybody is a bit more relieved, but that's not the case for SMT yet.
>
> Just my 2 cents,
>
> Mate
>
>
> [1] https://gcc.gnu.org/bugzilla/show_bug.cgi?id=47365
> [2] http://www.msoos.org/2013/04/gcc-4-5-2-at-sat-competition-201/
> [3] http://www.cs.utexas.edu/~marijn/drat-trim/
>
>
> _______________________________________________
> SMT-COMP mailing list
> SMT-COMP at cs.nyu.edu
> http://cs.nyu.edu/mailman/listinfo/smt-comp
>
>