[Termtools] fp, lp & relative srs

[Peter Schneider-Kamp]

Dear all,

inspired by the evaluation of the recent SAT competition,
I have taken the liberty of presenting the results of these
three finished categories through scatter plots.

In these plots, the x-axis represents the number of examples
where the tool could give an answer (YES+NO) while the y-axis
represents the time needed.

For example, if there is a mark for tool TALP at x=150
with y = 2.5, then TALP can solve 150 examples in at most 2.5
seconds.

These kinds of plots are nice to compare the performance of
tools w.r.t. efficiency and power. If one looks at lp.png
for example, one can draw the following conclusions:
* TALP is fast on easy examples, but not very powerful
* Polytool is much more powerful, albeit a bit slower than TALP
* AProVE is slowest, but by far the most powerful tool

Regards,
Peter
-------------- next part --------------
A non-text attachment was scrubbed...
Name: fp.png
Type: image/png
Size: 5564 bytes
Desc: not available
Url : http://lists.lri.fr/pipermail/termtools/attachments/20070605/653d8118/fp-0001.png
-------------- next part --------------
A non-text attachment was scrubbed...
Name: lp.png
Type: image/png
Size: 12753 bytes
Desc: not available
Url : http://lists.lri.fr/pipermail/termtools/attachments/20070605/653d8118/lp-0001.png
-------------- next part --------------
A non-text attachment was scrubbed...
Name: srs-relative.png
Type: image/png
Size: 8608 bytes
Desc: not available
Url : http://lists.lri.fr/pipermail/termtools/attachments/20070605/653d8118/srs-relative-0001.png