enforcing witnesses

Skip to first unread message

Armin Biere

Nov 21, 2011, 8:49:48 AM11/21/11
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?


Jason Baumgartner

Nov 21, 2011, 1:26:13 PM11/21/11
to hw...@googlegroups.com
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.
Reply all
Reply to author
0 new messages