[Termtools] timing

[Johannes Waldmann]

Here is another point that I think should be made
more precise for next year: timing.

This is important for provers (combinators)
that plan to spend e.g. half of their time on some method A
and then the rest on method B.

The current rules say "use 60 (resp. 300) seconds"
but it is not made clear whether this referes to
"real time (wall clock)" or "CPU time (per process)".

Matchbox is being cautious and assumes wall clock time
internally. I think Jambox also does (e. g. we both use
the "timeout" command to kill SAT solvers and this uses the wall clock).
What does TTTbox do? (It seems to know very exactly what time it is,
so it can print DONTKNOW at the very last moment :-)

The problem with using wall clock is that other processes
might be "stealing" time. E.g. look at
http://www.lri.fr/%7Emarche/termination-competition/2006/webform.cgi?command=viewres&tool=matchboxsatelite&prob=SRS.Bouchare.01.srs
This consumed 20 seconds on the wall clock,
but Claude measured 10 seconds on the cpu clock.
Or is this the difference just the time for the SAT solver?

It would be natural to have only a cpu clock limit
but e.g. CASC also has a wall clock limit
which is twice the cpu clock limit. See "Resource Limits" in
http://www.cs.miami.edu/~tptp/CASC/J3/Design.html

PS: Speaking of resource limits, the other interesting resource is
of course space, and here I critize that the amount of available
space (physical RAM) was not published before the competition.

PPS:
It seems the extended timeout allows some additional matrix proofs:
http://www.lri.fr/%7Emarche/termination-competition/2006/webform.cgi?command=viewres&tool=jambox&prob=SRS.Waldmann.rbeans.srs
http://www.lri.fr/%7Emarche/termination-competition/2006/webform.cgi?command=viewres&tool=multumnonmulta&prob=SRS.Waldmann.r10.srs
That is indeed very interesting.
-- 
-- 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