[SMT-COMP] SMT-COMP 2019: Call for Comments, Benchmarks, Solvers

[Aina Niemetz]

Hi Mohamed,

sorry for the delay!
This is a great idea and we're happy to implement it!

> Of course, the solvers' answers should not conflict for (1)
> and (2). Otherwise, the benchmark should be discarded for the
> corresponding sub-track.
Indeed.

Thanks for your feedback!

Aina


On 1/23/19 7:17 AM, Mohamed Iguernlala wrote:
> Hi,
> 
> We would also suggest to add three sub-tracks to 'Single Problem
> Track' (formerly 'Main Track'):
> 
> This will not require extra resources, but just some
> scripts. Assuming a category 'C' of this track, once all the
> solvers have been ran on the benchmarks in 'C', one could
> classify the solvers using three criteria to identify:
> 
> (1) the best solver answering 'unsat'
> (2) the best solver answering 'sat'
> (3) the best solver overall
> 
> Of course, the solvers' answers should not conflict for (1)
> and (2). Otherwise, the benchmark should be discarded for the
> corresponding sub-track.
> 
> This distinction is already used in the SAT competition, but not
> in SMT. We think that it's very important in practice, because
> the techniques used to prove unsatisfiability may be different
> from those used to show satisfiability. For instance, some
> solvers always answer "unsat", "unknown" or "timeout", but
> never "sat".
> 
> Best regards,
> 
> Mohamed Iguernlala.
> 

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 488 bytes
Desc: OpenPGP digital signature
URL: </pipermail/smt-comp/attachments/20190128/d660b017/attachment.asc>