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

[Tjark Weber]

Giles,

On Fri, 2016-05-13 at 14:39 +0000, Giles Reger wrote:
> In experiments we solve many problems with an unknown status and find
> the notion of restricting the competition to only those with a known
> status to be at odds with the overall aim here: to solve hard
> problems efficiently.
> 
> We are more familiar with how the CASC competition is organised where
> (i) All solvers are run on all problems (with competition timing, not
> an inflated time limit) to establish status (rating in CASC)
> (i) All solvable problems (by anybody) are eligible for the
> competition
> 
> It seems that requiring two solvers to agree on the status of a
> benchmark does not encourage finding new ways to solve problems but
> only solving problems solvable by others.

I understand your point of view. Indeed, the current rules disadvantage
solvers that can solve benchmarks not solvable (with a much higher time
limit, nonetheless) by any other solver.

But historically, SMT-COMP has valued correct answers much more highly
than incorrect answers. Certainly returning an incorrect answer does
not amount to solving the benchmark. If a single solver's answer
suffices, how can we be confident that the answer is correct?

(It appears to me that the CASC system could potentially be gamed by a
wrapper script that runs last year's best solver, and arbitrarily
returns "sat" or "unsat" if the solver times out.)

Opening up SMT-COMP to benchmarks with unknown status would, at the
very least, require us to redefine when an answer is (in)correct. I am
happy to have an open-minded discussion about this, but I do not think
it would be appropriate to make such a substantial change on short
notice (i.e., for SMT-COMP 2016).

Best,
Tjark