SAT Race 2019

Mandatory participation requirements for SAT solvers

1. The source code of submitted SAT solvers must be made available (licensed for research purposes). The open source policy is strict: any submission that contains binary code will be disqualified.
2. A 1–2 page system description document (see below for details).
3. The co-authors of a solver in the solver description must match the co-authors listed in the submission system.
4. SAT solvers must conform to DIMACS input/output requirements (see SAT Competition 2009 for details).
5. Printing models in case of a satisfiable instance, as well as UNSAT certificates (proofs) in case of an unsatisfiable one, are required.
6. The certificates for UNSAT instances are to be produced in the DRAT (Delete Resolution Asymmetric Tautologies) format which is backwards compatible with the DRUP format of SAT Competition 2013.

System Description Document

Each entrant to the SAT Race 2019 must include a short (at least 1, at most 2 pages) description of the system. This should include a list of all authors of the system and their present institutional affiliations. It should also provide details of any non-standard algorithmic techniques (e.g., heuristics, simplification/learning techniques, etc.) and data structures, as well as references to relevant literature (be they by the authors themselves or by others). The system description must be formatted in IEEE Proceedings style, and submitted as PDF. The system descriptions will be included in a booklet that will be made available on the SAT Race 2019 website.

Ranking

Solvers are ranked using a PAR-2 score based on a 5000 seconds timeout.

Participation of Portfolios

By a portfolio SAT solver we mean a combination of two or more (core) SAT solvers developed by different groups of authors. Participation of portfolio SAT solvers is not allowed.

The reason for this rule is twofold. The first is to prevent participants to only implement an algorithm selection tool that calls existing solvers by other authors. Although research in algorithm selection is useful, it is not the focus of the SAT Competitions and Races. Second, we would like to encourage the SAT community to invest more effort into developing new solver code bases and thus to counter the current trend in which the vast majority of solvers is built on top of MiniSAT.

Qualification

There will be no qualification round, but only a testing round to ensure that solvers are running properly on the evaluation system. The test set of instances will consist in a random selection of instances from the last SAT Competitions. The organizers reserve the right to disqualify poorly performing solvers.

Disqualification

A SAT solver will be disqualified if the solver produces a wrong answer. Specifically, if a solver reports UNSAT on an instance that was proven to be SAT by some other solver, or it reports SAT and provides a wrong certificate. A solver disqualified from the competition is not eligible to win any award. Disqualified solvers will be marked as such on the competition results page.

Note that there is a dedicated period when the participants can check their results to ensure that no problems are caused by the competition framework.

Withdrawal

A solver can be withdrawn from SAT Race 2019 only before the deadline for the submission of the final versions. After this deadline no further changes or withdrawals of the solvers are possible.

Participation of the organizers

The organizers of SAT Race 2019 are not allowed to compete.

Number of submissions

Each participant is restricted to be a co-author of at most four different sequential solvers. Two solvers are different as soon as their sources differ or the compilation options are different. Solvers are also different if they use different command line options.