Shortcut: direct links to the selection of Application benchmarks and Crafted benchmarks. You can also reproduce the selection yourself!.

Random Category

The random benchmarks have been generated using a uniform random K-sat instance generator following the guidelines published by Oliver Kullmann for the SAT 2005 competition.

The instances are generated in both medium and large size. Medium benchmarks target complete solvers while large benchmarks target incomplete solvers. For each medium tuple of parameter (clause length, number of variables, ratio), 100 instances have been generated randomly. The 2007 winner of the random SAT category, gNovelty+, was used to descriminate between SAT and unsat benchmarks. The benchmarks found SAT be gNovelty+ (usually in a few seconds) were classified as SAT while the others were classified as unknown (probably UNSAT). Once classified that way, 10 SAT and 10 UNKNOWN benchmarks were selected per tuple of parameter. For large benchmarks, the instances have been generated slightly below the threshold, so they are probably SAT. We generated 100 of them, among which 10 where randomly selected per tuple of parameter.

The rationale was to have as many SAT than UNKNOWN benchmarks for complete solvers and as many UNKNOWN as large probably SAT benchmarks, i.e. specific benchmarks for complete and incomplete solvers.

After the first stage on random category, it appeared that the incomplete solvers were able to solve basically all the large instances for K=3. So, in agreement with the judges, it was decided to add larger benchmarks (followed by a star) to challenge the solvers during the second stage.

General principles adopted by the judges

No more than 10% of the benchmarks should come from the same source.

It was decided to build a set of 300 instances. As a consequence, no more than 30 benchmarks could be accepted per source.

The final selection of benchmarks should contain 45% existing benchmarks and 55% submitted benchmarks.

As a consequence, the final set of 300 benchmarks should contain 165 submitted benchmarks and 135 existing benchmarks.

The final selection should contain 10% easy, 40% medium and 50% hard benchmarks.

As a consequence, among the 135 existing benchmarks, we should have exactly 13 easy, 54 medium and 68 hard benchmarks while among the 165 submitted benchmarks we should have exactly 17 easy, 66 medium and 82 benchmarks.

Duplicate benchmarks found after the selection was done will simply be removed from the selection. No other benchmarks will be added to the selection.

As a consequence, the final set of benchmarks will be less than 300 benchmarks.

Application Category

In the case of the application category, the benchmarks are coming from several sources:

Existing Benchmarks

are comming from the two SAT Races (2006 and 2008) plus the SAT 2007 competition, industrial division.

Submitted Benchmarks

are the benchmarks submitted for the SAT competition 2009.

Note that the IBM benchmarks disappeared from the existing benchmarks because they are no longer available from IBM web site.

The benchmarks have been classified as EASY/MEDIUM/HARD benchmarks according to the results of the two winners of the SAT07 competition, industrial category (RSAT and PICOSAT), plus the widely used Minisat. Since those three solvers participated to the 3 competitive events, we simply used the publicly available results to classify the benchmarks.

easy

Solved within 30s by all the solvers.

hard

Not solved by any of the solvers within the timeout of the event (first stage for the SAT competition 07).

medium

The remaining instances.

Note that such definition is relative to the best solvers in 2007 for that category. As a consequence, some SAT solvers might find hard to solve some benchmarks classified easy while others may be able to solve some hard benchmarks in reasonable time.

The number of instances submitted by a given source ranged from 10 to 96. Thus it was not possible to accept as is all the submissions. Limiting the number of instance to 30 at most per submitter changed a bit the landscape:

Finally, once the pourcentage of existing/submitted and easy/hard/medium benchmarks are applied, we end up with the following selection of benchmarks for the competition:

During the selection of benchmarks, the initial set of benchmarks did contain several duplicated benchmarks. This was discovered once the benchmarks were added to the competition system because several statictics regarding the benchmarks are automatically computed. manol-pipe-f9b.cnf and manol-pipe-g10nid.cnf appeared both in HARD and MEDIUM category, post* benchmarks submitted to the SAT09 competition were exactly the ones used during the SAT RACE08. (we simply removed holes in variable numbering). It was decided to remove those duplicate benchmarks from the selection, without adding new ones.

Crafted Category

For the crafted category, the selection of benchmarks was make from the SAT07 benchmarks, crafted category (that contained a selection of benchmarks from all the previous competitions.

We followed the same principle as for the application category. The SAT solvers choosen to evaluate the difficulty of the benchmarks are the winners of the 2007 competition (March-KS and Satzilla-Crafted, plus Minisat 2007 that would have been the winner of that category using this year scoring scheme.

Following the rule applied for the application category, no single source should have more than 30 benchmarks. The updated numbers follows.

Among those benchmarks, 300 were randomly selected to match the ratios of easy/medium and hard decided by the judges.

Errata: it happened that 3 benchmarks were wrongly added twice to the selection (because they matched two different regular expressions used to classify the benchmarks). Those benchmarks are contest04-connm-ue-csp-sat-n800-d0.04-s362703357.sat05-548.reshuffled-07.cnf, contest04-connm-ue-csp-sat-n600-d0.02-s1676244754.sat05-535.reshuffled-07.cnf,contest03-SGI_30_50_30_20_3-dir.sat05-440.reshuffled-07.cnf.
Furthermore, the parity-games generator provides exactly the same benchmark for n=2,i=2 with or without the ce and ci parameters. As such, the instance_n2_i2_pp_ci_ce.cnf benchmark has been removed too from the selection.
The Q32inK08.cnf benchmark from the RamseyCube family was wrongly encoding the very same problem as Q3inK09.cnf so it as been removed as well.
Finally, the sgen generator submitted to the 2009 competition contains in fact two generators: one for satisfiable benchmarks, and one for unsatisfiable benchmarks. Only the satisfiable generator was new, the unsat generator is exactly the same as the SAT2007 competition. Therefore, the SAT07 and SAT09 unsat sgen benchmarks should be considered to come from the same source. It means that all (14) the SAT07 benchmarks from Ivor Spence should be removed to follow the rule that no more than 30 benchmarks should come from the same source.
The final selection without duplicates is thus a set of 281 benchmarks.