Benchmark Selection

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.

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. (For SMT-COMP 2009, these numbers are halved for QF_IDL to ensure a timely end to the competition.) In each category, the script selects (when possible) 25% easy-sat, 25% easy-unsat, 25% hard-sat, and 25% hard-unsat. A benchmark is easy if it has difficulty 0, 1, or 2. A benchmark is hard if it has difficulty 3, 4, or 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.

In QF_UFLRA there are only random benchmarks; in this case random benchmarks are allocated all 200 slots.

More detail on this procedure is included in a comment at the top of the source file.

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.
• smtcomp2009-benchs.txt: these are the eligible 2009 benchmarks for inclusion. This file lists SMT-COMP 2009 benchmarks and their metadata; the file format is described in the C source above. Download.
• smtcomp2009-allbenchs.txt: this is the total list of 2009 benchmarks, including ineligible benchmarks. Not yet available.

Last modified: Tue 17 Feb 2015 15:03 UTC