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

[Tjark Weber]

Mate,

On Wed, 2015-03-18 at 13:47 +0100, Mate Soos wrote:
> On 02/08/2015 04:18 PM, Tjark Weber wrote:
> > - Sequential vs. parallel performance: All solvers will have several
> > CPU cores available, and we plan to measure CPU and wall time. Solver
> > developers might wish to prepare both sequential and parallel versions
> > of their solvers.
> 
> So there will be 2 tracks, one parallel one sequential?

The current plan is to run each solver (on each benchmark) only once,
but to evaluate according to two different metrics (taking into account
either CPU time or wall time).

> How many CPU cores for the parallel? 2? 16? 32? Memory limit should
> probably be higher for the parallel? Or not?

Machine specs are published at
http://smtcomp.sourceforge.net/2015/specs.shtml

Solvers will have 4 cores and around 60 GB of memory available.

> Along the same lines: what timeout will there be? Wall clock timeout for
> parallel I guess?

The precise time limit is yet to be determined; it is likely around 40
minutes of wall-clock time (implying a CPU time limit of 160 minutes
for parallel solvers).

> How will perf be compared for parallel? sum(cpu time)/numcpu or
> wall-clock time? If there is contention on locked stuff these may be
> very different.

It seems to me that wall-clock time is the more relevant metric for
parallel solvers (also note that we measure CPU time for the sequential
evaluation already). However, comments on this are welcome.

> Further, roughly what timeouts are planned to be used (i.e. how many
> minutes)? Maybe there could be 2 tracks, one with shorter one with
> longer timeouts? (naturally, only needs to run 1x but would deal out 2
> awards) Some users are very time-conscious (10s is much too long), some
> are not (10 minutes is fine).

We (the SMP-COMP organizers) had already discussed this idea in the
wake of SMT-COMP 2014. Personally, I am very open to a "lightning
track". However, user requirements differ substantially. Comments on
what would be a good time-out value (or more generally, a good
evaluation metric) for such a track are welcome.

Best,
Tjark