Benchmark Selection

Benchmark Attributes

The benchmark selection program is somewhat different from last year's. It uses the status, difficulty, and category of the benchmarks, but doesn't read them from the benchmark files themselves. Rather, this information is extracted from a MySQL database used for SMT-COMP'07, and a benchmark selection program is run on this extracted metadata to form the final list of selected benchmarks.

The metadata differs from the values encoded in the benchmark files in three ways:

• Where the status encoded in a benchmark file is “unknown” but we can verify that the benchmark is in fact satisfiable or unsatisfiable.
• Where the category is missing from the benchmark file (as it is in some of QF_UFIDL's uclid benchmarks).
• Where the difficulty in the benchmark file is obsolete. The difficulty values have been recomputed for SMT-COMP'07 (based on the SMT-COMP'06 solvers Ario 1.2, Barcelogic 1.1, CVC, CVC3, HTP, MathSAT 3.4, Sateen, and Yices 1.0). For the new divisions QF_BV and QF_AUFBV, difficulty values have been estimated rather than computed.

Selection Algorithm

For each division, the check benchmarks are always included. In addition, the selection script will randomly select 100 benchmarks from each division with the following distribution (when possible): 85 industrial, 10 crafted, and 5 random. 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.

More detail on this procedure is included in a comment at the top of the source file, and in the rules PDF for this year's competition.

The actual benchmarks selected for competition this year are listed on the selected benchmarks page.

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.
• smtcomp2007-benchs.txt: input to the above script. Some changes may be made before the final selection, and the official input file will be posted here then. This file lists SMT-COMP'07 benchmarks and their metadata; the file format is described in the C source above. Download.

Last modified: Tue 17 Feb 2015 14:58 UTC