SAT Competition 2016

Mandatory participation requirements for SAT solvers

  1. The source code of submitted SAT solvers must be made available (licensed for research purposes) except for the solvers participating only in the No-Limits Track.
  2. A 1-2 page description (IEEE format) must be submitted together with the solver (see template) The description should be submitted in a zip or tar file containing the latex sources AND the pdf.
  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). Printing models in case of a satisfiable instance is required for all tracks expect for "no-limits". Additionally, UNSAT certificates (proofs) are required for the main tracks.
  5. SAT solvers that are planning to participate in the Main track must be able to produce certificates for UNSAT instances in tracecheck or DRAT (Delete Resolution Asymmetric Tautologies) format which is backwards compatible with the DRUP format of SAT Competition 2013.

Participation of Portfolios

By a portfolio SAT solver we mean a combination of two or more (core) SAT solvers developed by a different group of authors. A portfolio SAT solver may participate only in the "No-Limits" track of the competition.

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 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 the SAT Competition 2016 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 Competition 2016 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 different parallel solvers, and one Glucose hack-track submission. 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. However, we make an exception for a command line option that enables emitting UNSAT proofs for the certified UNSAT tracks. Authors can select per solver whether to participate in a track or not.