SAT Competition 2009: requirements for the solvers

Last update: $LastChangedDate: 2009-02-09 09:51:49 +0100 (lun. 09 févr. 2009) $.

Randomness and pseudorandomness

Randomness is not permitted. Each solver should produce repeatable results when run on the same input formula with the same conditions of time and space availability. Pseudorandomness is perfectly acceptable if the program controls it by specifying a random seed whose calculation is repeatable under the same conditions as just mentioned (see RANDOMSEED below).

Competition platform


The competition (main track) will run on the cluster provided by CRIL. On this cluster, nodes are all identical: Bi-Xeon 3 GHz with 2GB RAM.
Some special tracks will probably run on other platforms (including the Linux-based LRI cluster) and a parallel computer with 16 cores and 68GB also provided by the LRI (available for the multithread track).


On the main track cluster, nodes are using one flavor of Red-Hat Linux.
Linux master0 2.6.9-22.EL.rootsmp #1 SMP Mon Oct 3 08:59:52 CEST 2005 x86_64 x86_64 x86_64 GNU/Linux

For C and C++ source submissions GCC version 4.3.2 will be used for compilation. No other versions are supported. You will need to 'port' your source code to be compilable under version 4.3.2 of GCC prior to submission. If you are aware of a specific problem occurring with that version of GCC, please contact the organizers.

A script or makefile should be provided in order to build the solver. Contestants are free to choose the compilation flags suitable for their solver. However, when possible the compilation flag '-static' should be used. We also recommend using '-O3 -fno-strict-aliasing -DNDEBUG'.

The solvers can be compiled either for 32 or 64 bits architecture. It is the responsability of the author to use either -m32 or -m64 to explicitely choose the architecture.

Solvers written in Java will run on Sun JVM 6 update 11 for 32 or 64 architecture (to be chosen by the submitter).

Machine architecture

Machine-independent source code is preferred. However, the competition will use clusters of recent Linux machines.

Execution environment

Solvers will run on a cluster of computers using the Linux operating system. They will run under the control of another program (runsolver) which will enforce some limits on the memory and the total CPU time used by the program. Solvers will be run inside a sandbox that will prevent unauthorized use of the system (network connections, file creation outside the allowed directory, among others).

Solvers can be run as either as 32 bits or 64 bits applications. If you submit an executable, you are required to provide us with an  ELF executable (preferably statically linked). Authors submitting solvers in source form will have to specify if it should be compiled in 32 bits or 64 bits mode.

Two executions of a solver with the same parameters and system resources must output the same result in approximately the same time (so that the experiments can be repeated).

During the submission process, you will be asked to provide the organizers with a suggested command line that should be used to run your solver. In this command line, you will be asked to use the following placeholders, which will be replaced by the actual informations by the evaluation environment.
Examples of command lines:
DIR/mysolver --mem-limit=MEMLIMIT --time-limit=TIMELIMIT --tmpdir=TMPDIR BENCHNAME
java -jar DIR/mysolver.jar -c DIR/mysolver.conf BENCHNAME
As an example, these command lines could be expanded  by the evaluation environment as
	/solver10/mysolver /tmp/file.cnf 1720968
/solver10/mysolver --mem-limit=900 --time-limit=1200 --tmpdir=/tmp/job12345 /tmp/file.cnf
java -jar /solver10/mysolver.jar -c /solver10/mysolver.conf /tmp/file.cnf
The command line provided by the submitter is only a suggested command line. Organizers may have to modify this command line (e.g.
memory limits of the Java Virtual Machine (JVM) may have to be modified to cope with the actual memory limits).

After TIMEOUT seconds have elapsed, the solver will first receive a SIGTERM signal from the controlling program to terminate the solver.

The solver cannot write to any file except standard output, standard error and files in the TMPDIR directory. A solver is not allowed to open any network connection or launch unexpected external commands.

The solver may also (optionally) use the values of the following environment variables:

The two functions below show how to obtain these informations in C.
* Return the path to the only directory where solvers are allowed to read or write files
* will return "/tmp" if this information is not available (e.g. outside the evaluation environment)
char *getTmpDir()
char *s=getenv("TMPDIR");

if (s==NULL)

return s;
* Return the limit corresponding to name
* or 0 if no limit is imposed (e.g. outside the evaluation environment)
* To be used with name="TIMELIMIT" or name="MEMLIMIT"
int getLimit(char *name)
char *value = getenv(name);

if (value == NULL)
return 0;

return atoi(value);

Input Format

The input file format will be in a simplified version of the DIMACS format

Output Format

We ask for the solvers to DISPLAY messages on the standard output that will be used to check the results.


There is no specific order in the solvers output lines. However, all lines, according to its first char, must belong to one of the following categories:

Buggy or not?

In the following cases a solver is considered buggy and will be returned to the author(s): For instance, if the solver crashes itself without giving any solution, it will not be strictly considered as "buggy" (even if this is due to some internal bug...), but its result will be considered as UNKNOWN and the maximum time allowed will be charged for it.