SAT-Race Logo

SAT Competition 2017

Overview
General Rules
Competition Tracks
→Submission
→Unsat Certificates
→Glucose Hack Subtrack
→Incremental Library Track
Benchmarks
Organizers
Related Events
Solvers
Results
Downloads

SAT Competition 2017

Description of Tracks

The following tracks will be featured in 2017 SAT Competition.
  1. Main Track is the track of sequential SAT solvers. We will use 300-600 benchmark problems, the time limit will be 5000 seconds. All solvers participating in the Main track are required to provide certificates in both SAT and UNSAT cases. For more information about the UNSAT certificates see this page.
    We encourage Glucose hack authors to participate in the main track. A prize will be awarded to the best Glucose hack (based on Glucose 3.0). For more detals plase see this page
  2. Random SAT Track is the track of SAT solvers good on randomly generated satisfiable instances.
  3. Agile Track is the track of simple fast SAT solvers with low overhead, suitable for solving large numbers of not too hard SAT instances.
  4. Parallel Track is the track of parallel SAT solvers designed for computers with multiple CPUs or CPU cores.
  5. No-Limits Track is a special track where solver source code and solution certificates are not required and portfolios of any nature are allowed. Only brand new benchmarks will be used in this track.
  6. Incremental Library Track is for incremental SAT solvers, click here for more details.

Printing a model in case of a satisfiable instance is required for all tracks expect for "no-limits". UNSAT certificates (proofs) are required only in the main tracks.

Execution Environment

All the tracks except for the Parallel Track and Incremental Library Track will be run on the StarExec cluster. The time limit for solving an instance will be 5000 seconds (in each track). The solvers will be allowed to use up to 24GB of RAM

The Parallel Track will be run on computers with Dual Socket Xeon E5-2690 v3 (Haswell) : 12 cores per socket (24 cores/node), 2.6 GHz processors and 64 GB DDR4-2133 (8 x 8GB dual rank x8 DIMMS) main memory. Hyperthreading is Enabled - 48 threads (logical CPUs) per node. Compute nodes lack a local disk, but users have access to a 32 GB /tmp RAM disk to accelerate IO operations. Note that any space taken in /tmp will decrease the total amount of memory available on the node. If 8 GB of data are written to /tmp the maximum memory available for applications and OS on the node will then be 64 GB - 8 GB = 56GB.

The Incremental Library Track will be run on computers with 2 x Intel Xeon X5355 2.66 GHz (4-Core) processors and 24GB of RAM.

Awards

In total we will distribute 19 prizes. One prize for the best Glucose hack and 3 prizes for each of the Main, Parallel, Agile, Random SAT, Incremental Library and No-Limits Tracks: