Home Intro Tools Specs Thanks SMT-LIB Previous

Benchmark set and difficulty measurements

The benchmarks used in the competition are selected from the SMT-LIB benchmark set. The complete set is reduced by a few restrictions:

For the last point a measurement of difficulty is needed. This is an approximate measure meant simply to make the competition more challenging. For 2014 we used the value of the fastest solver on that benchmark in the 2013 evaluation. For benchmarks introduced since then, an approximate value was determined by taking the best value from running one or more solvers from the evaluation during the preparation for the 2014 competition.

The table from which benchmarks will be chosen for the competition is available here. The table will be updated during the course of preparing for the competition as benchmarks are corrected, removed because they are ill-formed or inappropriate, moved among logics as needed, or difficuly or expected results determined.

The table is in space-separated form that is very amenable to text processing tools such as awk, grep and sort. You can turn it into a comma-separated table for Excel or similar tools by using sed or tr to turn spaces into commas.

The columns in the table are these:

Home Intro Tools Specs Thanks SMT-LIB Previous

Last modified: Tue 17 Feb 2015 15:00 UTC
Valid XHTML 1.0 Valid CSS!