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:
- SATTIMEOUT (the number of seconds it will be allowed to run),
- SATRAM (the amount of RAM in Mb available to the solver).
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
- The file can start with comments, that is lines begining with the
character c.
- Right after the comments, there is the line
p cnf nbvar nbclauses indicating that the
instance is in CNF format;
nbvar is an upper bound on the
largest index of a variable appearing in the file;
nbclauses is
the exact number of clauses contained in the file.
- Then the clauses follow.
Each clause is a sequence of distinct non-null numbers between
-nbvar and nbvar ending with 0 on the same line;
it cannot contain the opposite literals i and -i simultaneously.
Positive numbers denote the corresponding variables.
Negative numbers denote the negations of the corresponding variables.
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:
- comments (any information that authors want to
emphasize, such like #backtracks, #flips,... or internal cpu-time),
beginning with the two chars "c "
- solution (satisfiable or not). Only one line of
this type is allowed. This line must begin with the two chars
"s " and must be one of the following ones:
- s SATISFIABLE
- s UNSATISFIABLE
- s UNKNOWN
- values of a solution (if any), beginning with
the two chars "v " (to be precised in the
following).
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:
- 10 for SATISFIABLE
- 20 for UNSATISFIABLE
- 0 for UNKNOWN
- any other error code for internal errors (considered as UNKNOWN)
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);
}
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).
- The answer and the error code are not coherent.
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.