Description of the Tracks

The competition will consist of multiple tracks, whereby a "track" is defined by a combination of

1. the type of solvers allowed to participate,
2. the computational resources provided to each solver, and
3. the class of benchmarks used.

The following taxonomy is followed:

Core solvers

• SAT Competition 2014 only allows submission of core solvers: solvers that use at most two different SAT solving engines for all runs and at any time during one category. Examples of core solvers are minisat, glucose, lingeling, SAT4J, clasp, CCASat, Sparrow, sattime and hybrid solvers like CCCeq. A preprocessor is not considered a solver so that a hybrid solver could additionally run a preprocessor. A portfolio approach consisting of only two different SAT solvers, each using one SAT engine, can also participate in this track.
  
  Note: the organizers and the judges of the competition reserve the right to make a final decision whether a particular solver is qualified to participate based on the above definition.

Computational resources (to be confirmed)

• Sequential -- 1 core (of a 6-core CPU), 11GB RAM, 5000 seconds CPU time, 50 GB /tmp disk space (100GB /tmp space for certified UNSAT track)
• Parallel -- 12 cores (of a cluster node), 22GB RAM, 5000 seconds wall-clock time, 100 GB /tmp disk space.

Classes of benchmarks

• Application (both SAT and UNSAT)
• Hard-combinatorial (both SAT and UNSAT)
• Random (both SAT and UNSAT)

Tracks

Using the above taxonomy, the following 13 tracks are organized for the SAT Competition 2014:

1. Sequential, Application SAT track.
2. Sequential, Application certified UNSAT track.
3. Sequential, Application SAT+UNSAT track.
4. Sequential, Hard-combinatorial SAT track.
5. Sequential, Hard-combinatorial certified UNSAT track.
6. Sequential, Hard-combinatorial SAT+UNSAT track.
7. Sequential, Random SAT track.
8. Sequential, Random certified UNSAT track.
9. Sequential, Random SAT+UNSAT track.
10. Parallel, Application SAT+UNSAT Track.
11. Parallel, Hard-combinatorial SAT+UNSAT Track
12. Parallel, Random SAT Track
13. Sequential, MiniSAT Hack-track, Application SAT+UNSAT track.

Benchmarks

The benchmark selection will be similar, but subject to changes, compared to SAT Competition 2013.

Evaluation - Ranking

The solvers will be ranked based on the number of instances solved using the provided computational resources. Ties will be broken by CPU time in sequential tracks, and by wall-clock time in parallel tracks. The instance is considered solved by a solver if the solver produced both the answer and the complete certificate within the allocated resources.

Awards

Tracks 1-9: 1st (SAT, UNSAT, SAT+UNSAT), 2nd (SAT, UNSAT, SAT+UNSAT), and 3rd (SAT, UNSAT, SAT+UNSAT).

Tracks 10-13: 1st, 2nd, and 3rd.

The first prize in each track is a silver medal. All co-authors of solvers that were ranked 1st, 2nd, or 3rd will receive a certificate.

The awards are subject to change in the tracks with a small number of participants. A gold medal will be awarded only if there are at least three solvers participating in the track. (for silver and bronze, respectively, four and five solvers need to participate).

Minisat hack track

This track, originally introduced for SAT Competition 2009 and had a follow-up during SAT 2011 and SAT 2013, is organized again. This year the latest release of Minisat (2.2.0) (the simp version) is used as the base solver.

The motivation of this track is twofold. On the one hand, we want to lower the threshold for Master's and PhD students to enter the SAT competition by bringing new and innovative ideas to the original Minisat solver. On the other hand, the aim is to see how far the performance of Minisat can be improved by making only minor changes to the source code. We strongly encourage usual participants to the main track (including non-students) with "hacked" Minisat solver to participate in this track.

Our motivation behind using Minisat as the base solver: Minisat is a well-known and widely adopted solver that can be seen as a canonical CDCL solver, offering an efficient (and necessary) CDCL basis and easily modifiable code. Indeed, Minisat has been often improved by introducing only minor changes to its code ("hacking it"). Furthermore, looking back at recent progresses in CDCL solvers, most of them are based on minor changes (<10 lines each): phase caching, blocked literals, and Luby series for rapid restarts.

The motivation behind competing with minor hacks is that it can help the community to detect which types of modifications pay off: in order to isolate the actual causes of improvements when modifying solvers, it is necessary to perform scientifically valid experiments on the effects of individual changes made to a solver (e.g., individual new techniques introduced to the base solver).

The organizers of the SAT Competition 2014 provide a patch for Minisat 2.2.0 that modifies the output following to the SAT Competition 2014 output requirements. Addionally, this patch enables Minisat to emit a proof in DRAT format for the certified UNSAT tracks. To patch Minisat, place the MinisatHack.patch file in the directory of Minisat and run: "patch -p1 < MinisatHack.patch".

The size of hacks is restricted as follows: the diff between the patched and modified sources of Minisat should be less than 1000 non-space characters. You can use our edit distance tool on all modified files to count the number of modifications, which summed up should be less than 1000.