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

[Mate Soos]

Hi,

On 05/13/2016 02:19 PM, David R. Cok wrote:
> The procedure in the past has been to run a set of solvers and to assign 
> a status if (a) all solvers producing a sat or unsat answer agree and 
> (b) at least two solvers produce a sat or unsat answer.
> 
> A couple years ago, after the competition in 2014, I, Aaron Stump, and 
> Clark Barrett ran a big job with a long time out (10 hours, I think) to 
> resolve the status of any benchmarks without a status. That task took a 
> few months, with the rate of progress depending on how many nodes Aaron 
> would let the task have. We succeeded on most but not all of the 
> outstanding unknown benchmarks. It would be straightforward to do so 
> again, but it does take some time.

I would like to say that it can be dangerous to do that. I remember this
one bug [1] in gcc that made all variants of MiniSat (essentially all
top SAT solvers except for lingeling) return the wrong answer for a
particular set of problems [2]. I know this sounds like the stuff of
nightmares, but it actually happened and affected all these solvers for
years. Nowadays we have proof verification in SAT [3] so I think
everybody is a bit more relieved, but that's not the case for SMT yet.

Just my 2 cents,

Mate


[1] https://gcc.gnu.org/bugzilla/show_bug.cgi?id=47365
[2] http://www.msoos.org/2013/04/gcc-4-5-2-at-sat-competition-201/
[3] http://www.cs.utexas.edu/~marijn/drat-trim/

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5524 bytes
Desc: S/MIME Cryptographic Signature
URL: </pipermail/smt-comp/attachments/20160515/f1d401f0/attachment.p7s>