SAT Competition 2016

Description of Tracks

The following tracks will be featured in 2016 SAT Competition.
  1. Main Track is the track of sequential SAT solvers. We will use 600 benchmark problems each belonging to one of six categories. These categories will be determined based on the nature of available benchmarks. The categories might be for example:
    • Software verification
    • Hardware verification
    • A.I. Apllications (planning, scheduling, ...)
    • Obstruction (small hard crafted problems)
    • Combinatorial Challenges
    • Theorem proving
    Each category will be represented by 100 instances half of which will be satisfiable. 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 25 prizes.

10 prizes for Main Track Participants:

3 prizes for each of the Parallel, Agile, Random SAT, Incremental Library and No-Limits Tracks (in total 15 prizes):