Welcome to the SAT Challenge 2012!
Affiliated with SAT 2012, June 17–20, Trento, Italy.

Overview

The SAT Challenge 2012 is a competitive event for solvers of the Boolean Satisfiability (SAT) problem. It is organized as a satellite event to the Fifteenth International Conference on Theory and Applications of Satisfiability Testing (SAT 2012) and stands in the tradition of the SAT Competitions that have been held yearly from 2002 to 2005 and biannually starting from 2007, and the SAT-Races held in 2006, 2008 and 2010.

The SAT Challenge differs from both previous SAT Competitions and SAT-Races. Similar to SAT Competitions, there will be several tracks suitable for different kinds of solving algorithms (e.g. complete or local search). Similar to SAT-Races, the time to solve each instance will be limited to 15 minutes, and the solvers' source code need not be made publicly available (although we encourage this).

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

The SAT Challenge 2012 will consist of 5 tracks, which are run independently:

3 Main Tracks for Sequential Solvers:
- Application SAT+UNSAT: problem encodings (both SAT and UNSAT) from real-world applications, such as hardware and software verification, bio-informatics, planning, scheduling, etc.
- Hard Combinatorial SAT+UNSAT: hard combinatorial problems (both SAT and UNSAT) to challenge current SAT solving algorithms (similar to the SAT Competition's category “crafted”)
- Random SAT: randomly generated satisfiable instances
1 Track for Parallel Solvers: Application SAT+UNSAT: Same problem instances as in the Application Main Track. Eight cores can be used.
1 Track for Sequential Portfolio Solvers: 1/3 Application SAT+UNSAT, 1/3 Hard Combinatorial SAT+UNSAT, 1/3 Random SAT+UNSAT: A portfolio solver is a solver which combines different (sequential) SAT algorithms. It may, e.g., run multiple solvers in a time-slicing manner on the given SAT instance, or select one solver out of a set of given ones (e.g., determined by a machine-learning approach based on some metric) to tackle the problem.

A solver may participate in multiple tracks. The organization committee reserves the right to restrict participation of a solver to certain tracks, and to allow only a limited number of solvers submitted by the same person. Solvers must provide a satisfying truth assignment for satisfiable instances.

Organization

Researchers from both academia and industry are invited to submit their solvers—in either source code or binary format—to the SAT Challenge 2012. All entrants will have to solve a set of benchmark instances in DIMACS CNF format that will be drawn randomly from a pool of instances. This pool will include benchmarks from previous SAT Competitions and SAT-Races, but may be extended with additional instances. The exact benchmark set will not be published in advance.

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

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

Contact