SAT-Race 2010

July 11–14, Edinburgh, Scotland, affiliated with SAT'10/FLoC'10

SAT-Race 2010 is a competitive event for solvers of the Boolean Satisfiability (SAT) problem. It is organized as a satellite event to the Thirteenth International Conference on Theory and Applications of Satisfiability Testing (SAT'10) and stands in the tradition of the yearly SAT Competitions that have been held since 2002 and the SAT-Races held in 2006 and 2008 in Seattle and Guangzhou. In contrast to the SAT Competitions, the focus of SAT-Race is on application benchmarks only. Moreover, the time to solve each instance is limited to 15 minutes.

Objective

The area of SAT Solving has seen tremendous progress over the last years. Many problems (e.g. in hardware and software verification) that seemed to be completely out of reach a decade ago can now be handled routinely. Besides new algorithms and better heuristics, refined implementation techniques turned out to be vital for this success.

To keep up the driving force in improving SAT solvers, we want to motivate implementors to present their work to a broader audience and to compare it with that of others.

Tracks

SAT-Race 2010 will consist of three tracks:

• Main Track: Sequential SAT solvers, input formulas in CNF (DIMACS format).
• Special Track 1: Parallel (multi-threaded) SAT solvers, input formulas in CNF (DIMACS format).
• Special Track 2: Structural SAT solvers, input formulas in AIG format.

Organization

Researchers from both academia and industry are invited to submit their solvers—in either source code or binary format—to SAT-Race 2010. During SAT-Race, all entrants will have to solve a set of benchmark instances in DIMACS CNF format (AIG format for Special Track 2) that will be drawn randomly from a pool of instances. This pool will mainly consist of benchmarks from previous SAT Competitions (industrial/application category) and SAT-Races, but may be extended with additional instances of industrial relevance. The exact benchmark set will not be published in advance; a set of similar benchmark instances will be made available for testing purposes, however.

For each instance and solver there will be a time limit of 15 minutes.

Solvers will have to qualify for SAT-Race 2010 by participating in a qualification round.

Assessment of solvers will be based on the number of successfully handled instances and the time needed to solve them.