Configurable SAT Solver Challenge (CSSC) 2013

Thanks to all participants! There now is a technical report with the results of CSSC 2013 and an arXiv paper about the CSSC.

Results

We configured each solver for each benchmark and measured its number of timeouts and runtime for solved instances (all on instances disjoint from those used for configuration). We simply summed these measures up across the benchmarks in each track, and for reference, also computed the same measures for the default performance. Here are the results:

These results show quite clearly that algorithm configuration has a major impact on the ranking of algorithms (e.g., neither of the top 3 solvers in the CSSC would have been in the top 3 had we only looked at default configurations). Here are the detailed measures for each benchmark, and here are scatter plots of test performance for default vs. optimized configuration (for each solver and each benchmark). 

Instances

We will shortly provide separate downloads for each of the benchmark instance sets.

CSSC directory structure

Here is the entire CSSC directory structure (with the exception of the instances, see above). This includes all solvers, configuration spaces, scenario files, configurators, and results.

Solver configurations

For each solver, we provide a file with the optimized configuration for each of the benchmarks. The configurations are given as a callstring that can be executed from the cssc directory structure. Each line is for one benchmark, with the first line being the default.

• Callstrings for clasp-cssc
• Callstrings for forl-nodrup
• Callstrings for gnovelty+GCa
• Callstrings for gnovelty+GCwa
• Callstrings for gnovelty+PCL
• Callstrings for lingeling
• Callstrings for riss3g
• Callstrings for sat4j
• Callstrings for simpsat
• Callstrings for Solver43
• Callstrings for riss3gExt (closed source)

Please send any questions, concerns or comments to cssc.organizers@gmail.com.