[Termtools] randomness and determinism

[Johannes Waldmann]

Dear all,

As Torpa does not evaluate the "timeout" command line parameter, see
http://www.lri.fr/~marche/termination-competition/2006/torpa/runme ,
my guess at why Torpa misses the SRS/Trafo-un17 proof
in the second stage is that it behaves non-deterministically.

I noticed before that Torpa's runtimes are sometimes not predictable.
Of course in 99 percent of all case, the runtime is
precisely 0.03 seconds but there are a few exceptions.
I just tried three times to run Torpa(-1.5) on the above problem
and in one case, it found a solution with 10 seconds,
on two other cases, no solution within one minute.

I think it would be very good to require (for future competitions)
that provers behave deterministically. Otherwise, the experiments
cannot be reliably repeated. But then we cannot draw reliable
conclusions either.

Of course some modules of some provers rely on "random" numbers.
It is not the intention to prohibit this.
The way this seems to be handled in other competitions (e. g. SAT)
(see "Technical Issues/Randomness and pseudorandomness" in
http://www.satcompetition.org/2005/whatsnew05.html)
is that provers *must* be deterministic but they are called
with an additional argument which is a random number that is
generated by the driver script. Provers can use this argument
to "seed" their pseudo-random generator. Of course
the competition organizer has to keep track of these seeds.

Best regards,
-- 
-- Johannes Waldmann -- Tel/Fax (0341) 3076 6479/80 --
---- http://www.imn.htwk-leipzig.de/~waldmann/ -------

_______________________________________________
Termtools mailing list
Termtools at lists.lri.fr
http://lists.lri.fr/mailman/listinfo/termtools