Submission Instructions

All sequential tracks will be run on the BenchCloud Instance of SoSy Lab in Munich using compute nodes with an 8 cores Intel Xeon E3-1230 v5 @ 3.40 GHz CPU. The solvers will be executed with a time limit of 5000 seconds and memory limit of 30GB.

Testing and Requirements

The solver should be able to be built and run on a system that conforms to the specification in the Computing Environment on Competition Machines section of the SoSy Lab Competition Scripts. The top-level directory of your solver should contain two scripts:

• build.sh, for building the solver.
  

  The build script should take no parameters and should be tested and work on the provided Docker image.

• run.sh, to run the solver.
  

  The run script should take two parameters: The first parameter is the path to the benchmark instance. The proof for UNSAT instances must be written to a file named proof.out and placed in the folder that your run script receives as the second parameter.

  Note that the answer line ("s SATISFIABLE" and "s UNSATISFIABLE") and the solution in case of a satisfiable instance (lines starting with "v") must still go to stdout (not to "proof.out").

Submission

The submission of the final version of a solver is via a private GitHub repository, which is to be made available to the organizers by the solver authors. After the solver submission deadline we will ask all the participants to make their repositories public.

Emailing your System Description Document

After you have submitted the final version of your solver send an email to the organizers (organizers@satcompetition.org) containing your system description document (see General Rules for more information).