Judging and Scoring

SMT-COMP will be overseen by a Competition Panel consisting of the organizers plus one distinguished researcher from outside the SMT community, to be invited by the organizers. This researcher will serve as chair of the Competition Panel. The chair is responsible for certifying, as far as possible, the fairness of the competition. The Competition Panel will be in physical attendance for the duration of SMT-COMP (from the beginning of competition July 6 until after the final results are announced July 10).

Winners in each Problem Division for which there are at least three entrants from distinct research groups competing will be taken to be those with the highest score, according to the system of points and penalties in Table below. As indicated, correct answers are awarded a positive number of points, while incorrect answers are penalized by assigning a negative number of points. In recognition of the greater difficulty of achieving completeness than soundness in SMT systems, smaller penalties are assessed for incompleteness than for unsoundness. The organizers take responsibility for determining in advance whether formulas are satisfiable or not. In the event of a tie in total number of points, the solver with the lower average CPU time on formulas for which it did not timeout will be considered the winner. For Problem Divisions with fewer than three entrants, the results will be reported but no winner officially declared.

Last modified: Tue 17 Feb 2015 14:59 UTC