[SMT-COMP] benchmark data
David Cok
dcok at grammatech.com
Mon Jun 9 12:34:06 EDT 2014
Per the rules, benchmarks are excluded if all solvers acting on them in
the SMT-EVAL-2013 run completed in less than 5 seconds. That is what is
meant in the table by trivial.
We are intending to include all the benchmarks we can, given the
resources. Our current estimates are that we can't quite do that for the
divisions with several thousand eligible benchmarks, but we are refining
our estimates of the average computation time to have a better sense of
what to expect. Also, as described in the rules, we will be dividing
large divisions into heats, and will execute as many heats as possible
before the end of the competition.
- David
On 6/9/2014 12:05 PM, Bruno Dutertre wrote:
> On 06/09/2014 07:27 AM, David Cok wrote:
>> SMTCOMP competitors:
>>
>> The current data on benchmarks for SMT-COMP 2014 has been posted to
>> http://smtcomp.sourceforge.net/2014/difficulties.shtml
>> Note the caveats about this data - we are still correcting errors in
>> the benchmarks, running trial runs to determine difficulty ratings,
>> and trial runs to determine sat/unsat status of (some of the)
>> currently unknown benchmarks. When benchmarks are updated the
>> benchmark ids change - to be using current benchmarks, you need to
>> recopy benchmarks into your trial spaces.
>>
>> Thanks for email pointing out mal-formed benchmarks. Those are being
>> corrected, primarily by Clark Barrett and Morgan Deters. Let us know
>> of others you find.
>>
>> Our initial capacity estimates indicate that for most of the
>> divisions, we will be able to run all of the eligible benchmarks
>> (those that are non-trivial and have a known status).
>> (With the reorganization of benchmarks, there are now many divisions
>> with <1000 benchmarks).
>>
>
> What's the definition of non-trivial? This seems highly subjective.
> If trivial implies easy, and you have enough resources, I don't see why
> you don't just include all the benchmarks with a known status.
>
> Bruno
>
More information about the SMT-COMP
mailing list