SAT Competition 2018

Affiliated with the 21th International Conference on Theory and Applications of Satisfiability Testing
taking place July 9 – July 12 in Oxford, UK.

The 2018 SAT Competition is a competitive event for solvers of the Boolean Satisfiability (SAT) problem. It is organized as a satellite event to the 21th International Conference on Theory and Applications of Satisfiability Testing and stands in the tradition of the yearly SAT Competitions and SAT-Races / Challenges.

New this year:

• All benchmarks will be modified by applying satisfiability preserving transformations. These transformations are intended to counter overfitting of solvers, while not destroying the general structure of the formulas. Details on the applied transformations will be made public, but only after the competition.

Same as last year:

• BYOB - Bring your own Benchmarks: each Main Track participant (team) is required to submit 20 new benchmark instances (not seen in previous competitions). At least 10 of those benchmarks should be "interesting": not too easy (solvable by MiniSat in a minute) or too hard (unsolvable by the participants own solver within one hour on a computer similar to the nodes of the StarExec cluster). See the benchmarks page for more information.
• The solvers will 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.

Further news:

• Participants are encouraged to also submit (variants of) their solvers to the coordinated Sparkle SAT Challenge 2018, a novel competitive event that leverages cutting-edge automatically constructed algorithm selectors to assess the state of the art in solving the Boolean satisfiability (SAT) problem, and to quantify contributions of individual solvers. The Sparkle challenge offers a chance for wide recognition for SAT solvers that perform well “across the board”, as well as for specialized solvers with excellent performance on specific types of instances. Details on the Sparkle challenge can be found here.

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 Competition 2018 will consist of the following tracks*:

• Main Track (with a Glucose-Hack award)
• Parallel Track
• Random Satisfiable Track
• No-Limits Track

* Tracks with less than 3 participants will be canceled.

Important Dates

Registration Opens:	1st March, 2018
Benchmark Submission Deadline	March 31, 2018 April 15, 2018
Solver Submission Deadline:	March 31, 2018 April 15, 2018
Announcement of Results:	At the SAT'18 Conference

Organization

Researchers from both academia and industry are invited to submit their solvers and benchmarks to SAT Competition 2018.