The 2019 SAT Race is a competitive event for solvers of the Boolean Satisfiability (SAT) problem. It is organized as a satellite event to the 22th International Conference on Theory and Applications of Satisfiability Testing and stands in the tradition of the yearly SAT Competitions / Races / Challenges. The deadline for submitting benchmarks and solvers is Monday April 15, 2019 (23:59 GMT -12, anywhere on earth). Visit the SAT Race website at http://sat-race-2019.ciirc.cvut.cz/ for details.

Benchmarks

We strongly recommend participants to submit benchmarks, although it is not mandatory this year. The availability of many new benchmarks instances will increase the quality of the SAT Race. Everyone is welcome to contribute benchmarks (also if no solver is submitted). The organizers prefer to have as many interesting benchmark submissions as possible. A benchmark is considered interesting if it is not too easy (solvable by MiniSat in a minute) or too hard (most solvers require many hours of solving time on a computer similar to the nodes of the StarExec cluster).

Solvers

The SAT Race consists of only one track, which is similar to the Main Track of the SAT Competitions. The solvers will be ranked using the PAR-2 scheme: The score of a solver is defined as the sum of all runtimes for solved instances + 2*timeout for unsolved instances, lowest score wins. Solvers must be submitted as source code only and the sources of participants will be released after the Race.

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.