enforcing witnesses

[Armin Biere]

Due to the glitch in the liveness track (see the update on the
results) it seems
to be time to enforce witnesses next year, at least in a mild form.
The most
strict rule would be the same as in the SAT competition. If no
witness is provided
for a satisfiable instance, the instance is not scored. A wrong
witness will
mark the model checker as buggy and it will not take part in the
official ranking.

Is this too strict?

Armin

[Jason Baumgartner]

While requiring a witness will help rule out tool errors, it may be
very hard to rule out incorrect unsatisfiable answers since their
solution may require a combination of transforms, BDD-based engines,
and SAT-based engines. I think that attempting to obtain known correct
results for the benchmarks would be valuable. I leave to Armin's
discretion if witnesses are to be required. I agree that this is
relatively easy way to rule out one class of tool problems, if the
tools owners are willing to provide them.