Testing Correctness

Correctness of generated answers will be checked by the evaluation environment, as far as possible. Indeed, not all answers given by a solver can be checked efficiently. Therefore, some answers given by a solver may be wrong but this may be unnoticed by the evaluation environment.

Here are the checks made for each answer:

• Witnesses (in case of satisfiable problems):
  Witnesses generated by a solver will be checked for correctness by a verifier program. This type of answers is the only for which correctness can be established with certainty.
• UNSATISFIABLE:
  The only check that is made is to verify that no other solver found a solution to this instance. An UNSATISFIABLE answer is not reliable. Some solvers may wrongly indicate UNSATISFIABLE, but unless another solver finds a model, this will remain undetected.
• UNKNOWN:
  Does not need to be verified.
• OPTIMUM FOUND:
  Beyond verifying the model and the value of the objective function, the only check that is made is to verify that no other solver found a better solution to this instance. An OPTIMUM FOUND answer is not reliable. Some solvers may wrongly indicate OPTIMUM FOUND but unless another solver finds a better model, this will remain undetected.