Results of the SAT 2005 competition
Download
You can download the industrial and crafted benhcmarks from our site.
Concerning the industrial benchmarks, you need to obtain Miroslav Velev and IBM benchmarks directly from their site (Miroslav Velev benchmarks are too big and IBM benchmarks are only available for researchers from academia).
- Random benchmarks (25 MB)
- Crafted benchmarks (360 MB)
- Industrial benchmarks (205 MB)
- IBM FV website: download benchmarks ....
- Miroslav Velev Benchmarks: download benchmarks ....
- A script to shuffle IBM benchmarks the same way it was done for the competition
- A script to shuffle Velev benchmarks the same way it was done for the competition
You can also download the raw results of the first stage or the raw results of the second stage. First stage
In the first stage, the timeout was 20 minutes per benchmarks.
Just click on the name of the benchmarks to see the series submitted.
Clicking on a series will show/hide the summary of the results for each benchmark of the series. Clicking on a benchmark name will show the detailed results per solver.
You can grad the 2 pages description of the solvers by clicking on the (PDF) link near the name of the solver. (www) links are appearing on the site, to allow you to download the source code of the solvers. We do prefer to let the aauthors manager the way they distribute their work to the community.
Figures
The following figures were presented during the SAT 2005 conference.
(click on a figure to enlarge)
Benchmarks size
The following diagrams (called "box-plots") do represent the size (in number of literals occuring in the benchmarks) of the series of benchmarks in each category.
While this is not very useful for the random category (since the size was always the same in a given category, they are interesting in the crafted and industrial categories.
Behavior of the solvers
Those curves are used to show the behavior of the solvers when the timeout is increasing.
Robust solvers should be able to solve more benchmarks (in abscisse) when the timeout (in ordinate) is growing.
Clustering of solvers
The solvers are grouped together if they behave similarly on a given set of benchmarks.
The figures also show for each cluster of solver the union and the intersection of the benchmarks solved.
Second stage
In the second stage, the timeout was 200 minutes per benchmarks in the industrial category, and 100 minutes per benchmarks in the random and crafted categories.
Note that only the solvers launched under the second stage conditions do appear.
We plan to run most of the competitors under the second stage conditions.
Note that here only the solvers selected for the second stage in a category are appearing, and that most solvers donot appear in all categories.
Some figures
Behavior of the solvers after the extended timeout.
The curves related to the timeout are very important, especially in the industrial category because the timeout in the second stage was one order of magnitude bigger than in the first stage.
The timeout of the first stage is shown as a dashed line. One can note that in many cases, the order of the solvers (by considering the number of benchmarks solved) does change when the timeout increases.
