Updated on March 19 with poll results. The login of the submitters that voted for a given scoring scheme is displayed to allow the submitters to check that their vote has been properly taken into account.

Lexicographical NBSOLVED, sum ti (9 votes)

sat09-18, sat09-25, sat09-22, sat09-33, sat09-24, sat09-43, sat09-21, judge1, sat09-46

Cumulative time based, with timeout penalty, PENALTY = 10 (3 votes)

sat09-30, sat09-13, sat09-28

Cumulative time based, with timeout and robustness penalties (4 votes)

sat09-19, sat09-17, sat09-45, sat09-37

The competitors are expected to vote for the ranking scheme that will be used during the competition. One vote per submitter (i.e. login). A submitter can propose alternative ranking schemes based on the data available in the competition framework. The submitter vote (preferred scoring scheme) is to send by email to organizers at satcompetition dot org.

Poll Important deadlines

March 11, 2009

Proposal of extra schemes.

March 18, 2009 (UPDATED, NOT ENOUGH VOTES ON MARCH 13)

Poll for the preferred scheme.

March 18, 2009

Poll for the constant

Rationale

We have heard at least two criticisms against the scoring scheme used in the previous competitions. First, it aggregates two criteria which are orthogonal, and second, the score of a solver depends on other solvers.

From a practical point of view, a standard user of SAT technology wants to identify the solvers which are the most likely to solve its instances. This corresponds to a notion of robustness. "Best" solvers are the ones which solve the greatest number of instances, preferably in the smallest time.

From a "scientific" point of view, the community would like to award an innovative solver. A solver which solves instances that other solvers don't (SOTAC) is an example of such kind of solvers.

The purse system mixes these two points of view in a single ranking, but not everybody agrees with that.

Especially, the purse system has a the side effect to make the scores (thus the ranking) of two solvers depend on the results of a third solver.

So the idea this year is that the score of a solver should not depend on other solvers. This score should only depend on the chosen benchmarks set, the chosen time and memory limits and the chosen hardware. Hence the name SATSPEC09 to indicate that anybody would be potentially able to compare his solver with the solver submitted to the competition using that score. It would also allow to score additional solvers such as all the winners of the previous competitions without changing the scores of the solvers of this year competition.

There are several criteria which can be used to compare solvers:

• the number of solved instances
• the time used to solve instances
• the number of instances solved by only one solver
• the diversity of solved instances
• ...

One interesting question is if the speed of a faster solver can compensate for its failure to solve an instance. For example, assume solver A can solver 100 instances in 1000s (cumulated time) and solver B can solve the same 100 instances in only 100s. At this point, solver B is clearly better than solver A. Now assume solver A can solve one more instance than B. Which solver is the best? The answer is probably not unique and certainly depends on the user's applications and expectations.

Possible scoring

The competition framework generates the following data:

NBTOTAL

Total number of benchmarks to solve

NBSOLVED

Total number of benchmarks solved within a given timeout

NBUNSOLVEDSERIES

Total number of set of benchmarks for which the solver was unable to solve any element.

TIMEOUT

Time allowed to solve a given benchmark

ti

Time needed to solve a given benchmark, within the time limit

PENALTY

Constant to use as a penalty for benchmarks not solved within the timeout

SERIESPENALTY

Constant to use as a penalty for a set of benchmarks in which all members cannot be solved by the solver.

Lexicographical NBSOLVED, sum ti

Since the first edition of the SAT Race, we have seen in many papers and presentations experiments made on the SAT Race benchmarks sets (100 benchmarks each). The tables are usually sorted lexicographically, first on the number of benchmarks solved, then on the cumulative CPU time needed to solve those benchmarks.

It is a simple ranking scheme, easy to reproduce, and that can be easily used by SAT solver developers to see where their solver stands among state-of-the-art SAT solvers by running their own solver of the set of benchmarks on computers similar to the ones used during the Races.

	(NBSOLVED, sum ti)

Note: in this scheme, a fast solver cannot compensate for its inability to solve an instance.

Cumulative time based, with timeout penalty

Another simple way to rank the solvers is simply to sum up the CPU times of the solver on the set of benchmarks, and to give a penalty when the solver times out or abort early.

	sum ti + (NBTOTAL-NBSOLVED)*TIMEOUT*PENALTY

Note: in this scheme, a fast solver can compensate for its inability to solve an instance. The value of PENALTY determines how faster a solver must be to compensate for the loss of an instance.

Cumulative time based, with timeout penalty, log based

The idea of that scoring is the same as the preceding one, but based on a log of each CPU time to score closely solvers running in the same order of magnitude.

	sum log10(1+ti) + (NBTOTAL-NBSOLVED)*log10((1 + TIMEOUT)*PENALTY)

The motivation for using a log is that human beings are probably more receptive to the log of a value rather than the value itsef (100s and 1000s makes a significant difference, 100s and 200s is not so different). The 1 is introduced to avoid negative score for timings below 1s. Of course, log₁₀((1 + TIMEOUT)*PENALTY) can be rewritten as log₁₀(1 + TIMEOUT)+log₁₀(PENALTY).

Note: in this scheme, a fast solver can compensate for its inability to solve an instance. The value of PENALTY determines how faster a solver must be to compensate for the loss of an instance. For example, if PENALTY equals 100, failing on an instance can be compensated if the solver is 100 times faster on another instance, or if it 10 times faster on 2 instances, and so on. Possible values for PENALTY are 10, 100, 1000, 10000.

Cumulative time based, with timeout and robustness penalties

Proposed by Marijn Heule

The rationale of that scoring scheme is that a robust solver, i.e. a solver able to solve a wide range of benchmarks, (it could also be called multi-purpose), should be better ranked than a solver very good on very specific benchmarks. To do so, we add a new penalty for each series (kind of benchmark) for which the solver has not been able to solve any member.

	sum ti + (NBTOTAL-NBSOLVED)*TIMEOUT*PENALTY + NBUNSOLVEDSERIES*SERIESPENALTY

Note: we could also use a log scale on those numbers.

SAT 2005 and 2007 purse based scoring, aka Allen's scoring

See Allen's scoring poster or the SAT competition 2007 rules for details

Note that the purse based system does not obey the SATSPEC09 spirit, since it is dependent of the set of solvers to be evaluated.

Note: the advantage (and disadvantage) of this scoring is that it agregates several criteria.

Example: value of the different scorings for the first phase of SAT 2007

Category "crafted instances" (CRAFTED)

Category "industrial instances" (INDUST)

Category "random instances" (RANDOM)