Benchmark Selection

The benchmark selector will likely be the same as the one used for 2010.

Benchmark Eligibility

First, benchmarks that are of unknown status are ineligible.

Benchmarks that are “too easy” are similarly ineligible. “Too easy” is understood to mean that all of last year's solvers can solve the benchmark correctly in 5 seconds or less. However, if removing such benchmarks leaves a division with fewer than 300 eligible (non-check) benchmarks, then the easiest benchmarks are removed until 300 non-check benchmarks remain.

The organizers reserve the right to remove from competition eligibility uninteresting or over-represented benchmarks.

Selection Algorithm

For each division, the check benchmarks are always included. In addition, the selection script will randomly select 200 benchmarks from each division with the following distribution (when possible): 170 industrial, 20 crafted, and 10 random. In each category, the script selects (when possible):

• 10% sat with difficulty on the interval [0,1].
• 10% sat with difficulty on the interval (1,2].
• 10% sat with difficulty on the interval (2,3].
• 10% sat with difficulty on the interval (3,4].
• 10% sat with difficulty on the interval (4,5].
• 10% unsat with difficulty on the interval [0,1].
• 10% unsat with difficulty on the interval (1,2].
• 10% unsat with difficulty on the interval (2,3].
• 10% unsat with difficulty on the interval (3,4].
• 10% unsat with difficulty on the interval (4,5].

If there aren't enough random and crafted, then the slack is “inherited” by the industrial category. It there aren't enough industrial, then the slack is “inherited” by the crafted category. As a last resort, and only if necessary (as in divisions with only random benchmarks), random benchmarks are allocated additional slots.

More detail on this procedure is included in a comment at the top of the source file. A less algorithmic description can be found in the official rules.

Tool Download

• select_benchmarks: given an input file of benchmarks, selects benchmarks according to the rules; statistics on stderr, benchmarks on stdout. Some changes may be made to this program before it is used officially for the competition benchmark selection; it is intended that these changes be limited to bug fixes, removal of obsolete debugging code, and documentation cleanups. Source.
• smtcomp2011-benchs.txt: these are the eligible 2011 benchmarks for inclusion. This file lists SMT-COMP 2011 benchmarks and their metadata; the file format is described in the C source above. Not yet available.
• smtcomp2011-allbenchs.txt: this is the total list of 2011 benchmarks, including ineligible benchmarks. Not yet available.

Last modified: Tue 17 Feb 2015 15:01 UTC

Last modified: Tue 17 Feb 2015 15:01 UTC