SAT-Race 2008

May 12–15, Guangzhou, P. R. China, affiliated with SAT'08

SAT-Race 2008 is a competitive event for solvers of the Boolean Satisfiability (SAT) problem. It is organized as a satellite event to the Eleventh International Conference on Theory and Applications of Satisfiability Testing (SAT'08) and stands in the tradition of the yearly SAT Competitions that have been held since 2002 and the first SAT-Race held in 2006 in Seattle. In contrast to the SAT Competitions, the focus of SAT-Race is on industrial 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

In SAT-Race 2008 there will be three different 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.
Each track is run independently. SAT Solvers registered for Special Track 1 automatically participate (as sequential solvers) in the Main Track.

Organization

Researchers from both academia and industry are invited to submit their solvers—in either source code or binary format—to SAT-Race 2008. During SAT-Race, all entrants will have to solve a set of benchmark instances in DIMACS CNF (or AIG) format that will be drawn randomly from a pool of instances. This pool will mainly consist of benchmarks from previous SAT Competitions (industrial category) and SAT-Race 2006, 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. We will also organize qualification rounds, where participation in at least one of them is mandatory to qualify for the SAT-Race.

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