SAT Competition 2002: requirements for the solvers
Please note that this is a working document so it is subject
to change.
Last modification: 28 January 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.