[Termination tools] Several issues

[H. Zantema]

On Thu, 14 Apr 2005, Jörg Endrullis wrote:

> > 1) first run each tool with a timeout of 5 seconds
> > 2) if no tool solved the pb within 1 second (not 5), rerun the tools which
> > were unsuccessfull with a timeout of 1 minute.
> > 3) if no tool solves the pb within 30 seconds, rerun the tools which
> > were unsuccesfull with a timeout of 5 minutes.
> 
> I would suggest another alternative. We could introduce an overall
> timeout (1 minute * number of problems). First we run the whole contest
> with a timeout of 10 seconds. After that we could rerun the tools on the
> problems they were unsuccessful with the timeout ((overall - spent) /
> (problems left)). This would encourage fast termination provers but
> allow to spent more time for a limited number of problems.

I do not expect any improvement if we would choose such complicated ways
of running the competition, compared to the one fixed one minute time-out
as we have now. Sure if there are hard systems that can only be solved in
several minutes it should be encouraged that these proofs become visible
in the competition results. But in my experience it is always the case that
if you have a system that can be solved in several minutes, then by 
slightly tuning the chosen heuristics towards the found solution, this 
solution is found in at most a few seconds. It will often be the case that 
particular systems can not be solved in a default setting in reasonable
time, but can be in a special setting of the tool. This will not be 
affected at all by stretching the meaning of "reasonable time".

So my conclusion after all this discussion is: let's keep the simple 
one minute time-out.
 
Best Regards,

		Hans Zantema.

+--------------------------------------+-----------------------------+
|                                      |                             |
|   Dr Hans Zantema                    |   Hoofdgebouw   kamer 6.73  |
|   Faculteit Wiskunde en Informatica  |   tel (040)2472749          |
|   Technische Universiteit Eindhoven  |   fax (040)2468508          |
|   Postbus 513     5600 MB Eindhoven  |   e-mail  H.Zantema at tue.nl  |
|   The Netherlands                    |   www.win.tue.nl/~hzantema  |
|                                      |                             |
+--------------------------------------+-----------------------------+