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

Hardware

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).

Software

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.

BENCHNAME will be replaced by the name of the file (with both path and extension) containing the instance to solve. Obviously, the solver must use this parameter or one of the following variants: BENCHNAMENOEXT (name of the file with path but without extension), BENCHNAMENOPATH (name of the file without path but with extension), BENCHNAMENOPATHNOEXT (name of the file without path nor extension).
RANDOMSEED will be replaced by a random seed which is a number between 0 and 4294967295. This parameter MUST be used to initialize the random number generator when the solver uses random numbers. It is recorded by the evaluation environment and will allow to run the program on a given instance under the same conditions if necessary.
TIMELIMIT (or TIMEOUT) represents the total CPU time (in seconds) that the solver may use before being killed. May be used to adapt the solver strategy.
MEMLIMIT represents the total amount of memory (in MiB) that the solver may use before being killed. May be used to adapt the solver strategy.
TMPDIR is the name of the only directory where the solver is allowed to read/write temporary files
DIR is the name of the directory where the solver files will be stored

Examples of command lines:

	DIR/mysolver BENCHNAME RANDOMSEED
	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:

TIMELIMIT (or TIMEOUT) (the number of seconds it will be allowed to run)
MEMLIMIT (the amount of RAM in MiB available to the solver)
TMPDIR (the absolute pathname of the only directory where the solver is allowed to create temporary files)

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)
    s="/tmp";

  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.

Messages

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:

comments ("c " lines)
These lines start by the two characters: lower case c followed by a space (ASCII code 32).
These lines are optional and may appear anywhere in the solver output.
They contain any information that authors want to emphasize, such as #backtracks, #flips,... or internal cpu-time. They are recorded by the evaluation environment for later viewing but are otherwise ignored. At most one megabyte of solver output will be recorded. So, if a solver is very verbose, some comments may be lost.

Submitters are advised to avoid outputing comment lines which may be useful in an interactive environment but otherwise useless in a batch environment. For example, outputing comment lines with the number of constraints read so far only increases the size of the logs with no benefit.

If a solver is really too verbose, the organizers will ask the submitter to remove some comment lines.
solution ("s " lines)
This line starts by the two characters: lower case s followed by a space (ASCII code 32).
Only one such line is allowed.
It is mandatory.
This line gives the answer of the solver. It must be one of the following answers:
- s SATISFIABLEThis line indicates that the solver has found a model of the formula, and in such a case, a "v " line is mandatory.
  This line must be output when the solver has found a model.
- s UNSATISFIABLE
  This line must be output when the solver can prove that the formula has no model.
- s UNKNOWN
  This line must be output in any other case, i.e. when the solver is not able to tell anything about the formula.
It is of uttermost importance to respect the exact spelling of these answers. Any mistake in the writing of these lines will cause the answer to be disregarded.
Solvers are not required to provide any specific exit code corresponding to their answer.

If the solver does not output a solution line, or if the solution line is misspelled, then UNKNOWN will be assumed.
values ("v " lines)
This line starts by the two characters: lower case v followed by a space (ASCII code 32).
More than one "v " line is allowed but the evaluation environment will act as if their content was merged.
It is mandatory when the instance is satisfiable.

If the solver finds a solution (it outputs "s SATISFIABLE"), it must provide a model (or an implicant) of the instance that will be used to check the correctness of the answer, i.e., it must provide a list of non-contradictory literals which, when interpreted to true, satisfies each clause of the formula. The list of literals must be ended by a "0" (zero) otherwise it will be assumed that the list is incomplete and the answer will be ignored. The negation of a literal is denoted by a minus sign immediately followed by the identifier of the variable. It is NOT necessary to list the literals corresponding to all variables if a smaller amount of literals suffices. The order of the literals does not matter. Arbitrary white space characters, including ordinary white spaces, newline and tabulation characters, are allowed between the literals, as long as each line containing the literals is a values line, i.e. it begins with the two chars "v ".
If the solver cannot provide such a certificate for satisfiable instances, then the author(s) are asked to Contact The Organisers; then the decision concerning the solver will be made (e.g., running the solver in the demonstration division).

Note that we do not require a proof for unsatisfiability. The values lines should only appear with SATISFIABLE instance.
For instance, the following outputs are valid for the instances given in example:
```
mycomputer:~$ ./mysolver myinstance-sat
c mysolver 6.55957 starting with TIMEOUT fixed to 1000s
c Trying to guess a solution...
s SATISFIABLE
v 1 2 -5 
v 4 -9 0
c Done (mycputime is 234s).

mycomputer:~$ ./mysolver myinstance-unsat
c mysolver 6.55957 starting with TIMEOUT fixed to 1000s
c Trying to guess a solution...
c Contradiction found!
s UNSATISFIABLE
c Done (mycputime is 2s).
```

Buggy or not?

In the following cases a solver is considered buggy and will be returned to the author(s):

It outputs UNSATISFIABLE for a satisfiable instance.
It outputs SATISFIABLE, but provides an incorrect model (or an incorrectly formatted model).

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.