We asked submitters to send benchmarks in DIMACS file format5. One of the ideas underlying this format is that benchmarks are in CNF and are easy to read (for instance, variables are already indexed by integers). Of course, generators of benchmarks were allowed, assuming that authors gave clues for the interesting parameters to use with.
The output format (printed by solvers) was detailed in our call for solvers6. Briefly, the idea was to allow any solver to print any ``comment'' line (any information judged as ``interesting'' by authors) and some special lines for automated interpretation purposes. Information lines are important if one wants to understand results and to be able to interpret the huge amount of data collected during the competition. The output format allows to print the answer (SAT, UNSAT or unknown), and requests a certificate if SAT was claimed. If no answer was (syntactically) found in the output (for instances if the solver crashed or was timed out), then unknown was assumed.