Re: [Smtcomp-discussion] [SMT-COMP] SMT-COMP 2017: Call for Comments, Benchmarks, Solvers
Tools and documentation of the annual SMT competition
Brought to you by:
webertj
From: Andrew R. <and...@gm...> - 2017-03-26 23:03:40
|
Hi Tjark, On Fri, Mar 24, 2017 at 6:13 PM, Tjark Weber <tja...@it...> wrote: > Andrew, > > Thank you for your feedback! > > On Thu, 2017-03-16 at 10:38 -0500, Andrew Reynolds wrote: > > > Regarding disagreements between solvers, last year, as I recall, there > > was a separate discussion period where most (or all) disagreements > > between solvers were resolved e.g. a developer would say "my solver > > was wrong for this one", etc. Perhaps the competition should: > > > - Run all benchmarks/solvers, note the set of unknown status > > benchmarks D that two solvers disagree on. > > - Have a rebuttal period where solver developers can justify their > > answers for benchmarks in D. > > - Based on discussion, set the status on benchmarks in D, and then > > compute the final scores. > > I am concerned about some of the practical implications of this > suggestion. Preliminary results would have to be available probably 1-2 > weeks earlier than in the past (to allow sufficient time for the steps > above); the competition would depend on status updates by the SMT-LIB > maintainers in a time-critical fashion; and solvers would be run > against one SMT-LIB release but scored against another. > > It's not impossible, of course. But given the size of the competition > (with more than 200,000 benchmarks and 1.5 M job pairs in 2016), these > issues have the potential to cause some headache. I would much prefer a > simpler scoring solution that doesn't involve manual review. > > Right, I understand this would be a challenge. The proposal I mentioned is more of a wish than a suggestion. :) > > (4) Scoring: > > > One thing that has bothered me in previous competitions is how overall > > scoring is computed with respect to wrong benchmarks. > > > Say I have logics A, B, C, D with weights 1, and I solve all > > benchmarks in A,B,C, but I get 3 wrong benchmarks in D. Then my > > overall score is: > > > 1 + 1 + 1 + -3*1 = 0 > > > I would prefer if wrong benchmarks were punished slightly less, so > > that if a solver gets *any* number of wrong benchmarks in a logic, > > then its overall score is negative of the weight of that logic, so > > instead I'd have: > > > 1 + 1 + 1 + -1*1 = 2 > > On the other hand, one might argue that an unsound solver should not be > trusted in any division. There is an even harsher alternative to the > current scoring rule that has been considered before: to disqualify > unsound solvers entirely. In other words, the current scoring rule > already is a compromise. > > Here, I would argue that the implementation of SMT solvers tends to be fairly modular, meaning that if an SMT solver gets a wrong answer for logic A, then the bug is very likely in the component that specifically handles A, and the solver is likely still sound for everything besides A. Historically, this has been the case for CVC4. In my recollection: SMT comp 2012 CVC4 had a wrong answer in QF_BV related to an unsound bit-vector rewrite, SMT comp 2012 CVC4 had a wrong answer in QF_LIA related to a bug the arithmetic theory solver, SMT comp 2016 CVC4 had a wrong answer in QF_NIA related to the encoding of QF_NIA constraints as QF_BV ones. In each of these cases, CVC4 was still (to my knowledge) sound for everything besides the logics that had the bug. Of course this is not guaranteed to be the case, there could be a solver with a bug that effects all logics, but this is much less likely. Let's consider another case: Logic A, B with weights 1,1. Solver X gets 1 wrong answer in both A and B, it's total score is -1*1 + -1*1 = -2 Solver Y solves all benchmarks in A, but gets 4 wrong answers in B, its total score is 1 + -4*1 = -3 Here, I would argue that Solver Y is the better solver: it is (likely) sound for logic A, whereas Solver X is definitely unsound for both A and B. However, Solver X wins because it got lucky that only 1 benchmark exercised its unsoundness in A and B, whereas Solver Y was unlucky and had 4. If instead we used a punishment of ( -1*weight ) for the logic regardless of #wrong benchmarks, Solver Y would have a total score of 0, and Solver X would still have -2, which I believe would be more appropriate. I would be interested to hear further opinions on this issue. How much > emphasis should the competition place on soundness of solvers? > > I do think it is very important, and I do believe that an unsound solver is worse than a solver that solves no benchmarks. My opposition is to multiplying by the #wrong benchmarks, since this skews the results unfairly. A punishment of -1*(weight of logic) is still very severe, but is more appropriate for overall score, in my opinion. Let me know what you think, Andy > Best, > Tjark > > > |