[SMT-COMP] Question about benchmarks with unknown status

[Morgan Deters]

Hi Alberto,

If you can demonstrate the (un)satisfiability of any of the
unknown-status benchmarks, please let us know.  We have, in fact,
determined the status of many of the benchmarks added to SMT-LIB
recently, though not all of them.

We plan to have updated benchmarks, with current status and difficulty
information, published by June 1.  They will also be available for
execution on SMT-Exec.

Currently, in QF_LIA/nec-smt/large, we know 888 to be SAT, 1117 to be
UNSAT, and 376 remain unknown.  In QF_IDL/schedulingIDL, we have 247
SAT, 31 UNSAT, and 2 remain unknown.  We may be able to determine a
few more in the next few days.

Thanks,
Morgan (also for Clark, Aaron, and Albert)

On Wed, May 28, 2008 at 2:25 PM, Alberto Griggio
<alberto.griggio at disi.unitn.it> wrote:
> Hello list,
>
> we're writing because we have a question about the candidate set of
> benchmarks for the upcoming SMT-COMP. According to the rules, only
> benchmarks with known status (sat/unsat) are eligible for the
> competition, and this definitely makes sense. However, a big portion of
> the new benchmarks recently added to the SMT-LIB are marked as unknown
> (for example, those in QF_LIA/nec-smt/large, or in
> QF_IDL/schedulingIDL). Therefore, we wanted to know whether there are
> any plans to try to determine their status, or if they will just be not
> taken into account for the competition. In our opinion, it would be
> important to have as many benchmarks as possible in the competition
> pool, so it should be tried to assign a status to the unknown
> instances. Of course, we are willing to help in this if needed.
>
> Best,
>
> Alberto, Anders, Alessandro and Roberto
>
> _______________________________________________
> SMT-COMP mailing list
> SMT-COMP at cs.nyu.edu
> http://cs.nyu.edu/mailman/listinfo/smt-comp
>



-- 
Morgan Deters
mdeters at gmail.com