Benchmark Selection

Benchmark Attributes

The benchmark selection script uses the following benchmark attributes:

• :status - specifies the benchmark result - possible values: unsat, sat, unknown.
• :difficulty - specifies how difficult a benchmark is - possible values: 0 (easiest), 1, 2, 3, 4, 5 (hardest).

  The score was computed using the formula (int)(5 * (1 - SOLVED/TOTAL)), where SOLVED is the number of SMT solvers that could solved the benchmark in 10 minutes, and TOTAL is the number of SMT solvers that were tried.

  The following tools were used to compute this attribute: Ario 1.1, Barcelogic, CVC, CVC Lite 2.0, MathSAT 3.3.1, Sateen, Simplics, Yices.

  In the quantifier division, some trivial benchmarks have difficulty -1, and will not be used in SMT-COMP.

  A different approach was used to compute the degree of difficulty in QF_UFBV[32] and AUFLIRA, because none of the solvers above support these divisions and/or the SMT-LIB extensions used.

• :category - possible values: industrial, crafted, random, check.
• industrial - come from a real application (e.g., WiSA benchmarks) and were produced by a tool such as bounded model checkers, static analyzers, extended static checkers, etc.
• check - are used to test specific features (e.g., integer completeness and big number support).
• random - are randomly generated (e.g., DTP benchmarks).
• crafted - all others - they are usually designed to give a hard time to SMT solvers (e.g., scheduling benchmarks).

Selection Algorithm

For each division, the check benchmarks are always included. In addition, the selection script will randomly select N benchmarks 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.

Tool Download

• bench_select: randomly select a subset of lines of a specified size from an ASCII text data file. Source, Linux Binary.
• select.sh: main (bash) script on top of bench_select. It displays statistics on the standard error, and the selected benchmarks in the standard output. Source.

Last modified: Tue 17 Feb 2015 15:01 UTC