SAT Competition 2003: requirements for the solvers

Please note that this is a working document so it is subject to change.

Last modification: 28 november 2002.

Machine architecture

Machine-independent source code is preferred. However, the competition will use clusters of recent Linux i686 (or equivalent AMD) machines.

Input Format

The SAT solver must read the SAT instance from a file given in parameter:

./mysolver myinstance
If a solver uses random numbers, it must accept a second seed parameter, where seed is a number between 0 and 4294967295, e.g.,
  
 ./mysolver myinstance 12345
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 could be repeated).

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

Those values can be read using traditional C functions:
/* To be used with "SATRAM" or "SATTIMEOUT" */
/* Return the limit or:
   -1 if the variable is not set
   0 if there was a problem in atoi (variable isn't a number) */
int getSATlimit(char * name) {
 char * value;
 
 value = getenv(name);
 if (value == NULL) return(-1);
 return atoi(value);
}

After SATTIMEOUT is elapsed, the solver will receive the SIGKILL signal from the controlling program. Under all circumstances, no results will be considered as valid after SATTIMEOUT is elapsed.

The solver cannot write to any files except standard output and standard error (only standard output will be parsed for results, but both output and error will be memorized during the whole competition process, for all executions).

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

c
c start with comments
c
c 
p cnf 5 3
1 -5 4 0
-1 5 3 4 0
-3 -4 0

Output Format

We ask for the solvers to DISPLAY messages on the standard output that will be used to check the results and to RETURN EXIT CODE to be handled by the SAT-Ex system. The output format is partly inspired by the previously defined DIMACS output specification and may be used to manually check some results.

Messages

There is no specific order in the solvers output lines. However, all line, according to its first char, must belong to one of the three following categories: When a solver answers UNKNOWN, it is charged with the maximum allowed time SATTIMEOUT.

Technically, the two first chars are important and must be strictly respected: scripts will use traditional grep commands to parse results (and at least to partition standard output).

If the solver does not display a solution line (or if the solution line is not valid), then UNKNOWN will be assumed.

Providing a model

If the solver outputs SATISFIABLE, it should 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 0-terminated sequence of distinct non-contradictory literals that makes every clause of the input formula true. 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 Laurent Simon directly; then the decision concerning the solver will be made (e.g., running the solver hors concours).

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 SATTIMEOUT fixed to 1000s
c Trying to guess a solution...
s SATISFIABLE
v -3 4
v -6 18 21
v 1 -7 0
c Done (mycputime is 234s).

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

Exit code

In order to automatically check the correctness of solver's answers, all solvers must also exit with an error code that must characterize its answer on the considered instance. This is done in addition to the automatic syntactic analysis of solver's output (results must be coherent, otherwise the answer is considered as BUGGY). We use the same conventions as in Satex. The error code must be: Typically, if the solver is written in C, and if SAT and UNSAT are constants, a solver can end with such lines:
if (result==SAT) {
 fprintf(stdout, "s SATIFIABLE\n");
 outputCertificate(stdout);         /* print an implicant */
 exit(10);
} else if (result == UNSAT) {
 fprintf(stdout, "s UNSATISFIABLE\n");
 exit(20);
} else {
 fprintf(stdout, "s UNKNOWN\n");
 exit(0);
}

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.