Techniques and Standards for Evaluating ATP Techniques and Implementations

Skip to first unread message

Geoff Sutcliffe

Jul 16, 2021, 9:43:07 AM7/16/21
to TPTP World
Hi all,

For those at the ARCADE workshop, I've started this conversation following Michael Rawson presentation and the discussion that followed. I'll add my thoughts later.



Armin Biere

Jul 16, 2021, 10:28:29 AM7/16/21
to TPTP World
Let me add to this discussion the links I provided in the Zoom chat:

which was the result of a similar but longer discussion at the POS'20 workshop:

which actually was captured on Video

This also contains some discussion why we came at the end to finally start something
like that (we were really kind of starting to feel bad about how evaluation are done in SAT'16).

The idea to organize this through GITHUB (from Daniel) is nice.


P.S.  The SAT manifesto is the result of the lightning talk of Kuldeep. I talked in that session on CDF vs. Cactus and
blamed Laurent Simon to have invented the Cacuts plot, but then during the talk had to learn that a CASC paper
with Geoff provided the original idea.

Armin Biere

Jul 16, 2021, 10:29:22 AM7/16/21
to TPTP World

We were asked for a citable version (by Springer) and put it on Zenodo too:

Michael Rawson

Jul 16, 2021, 1:15:19 PM7/16/21
to TPTP World
Hi all,

Thanks for your input and support! I've made to collect all of your ideas. Go mad, we can make it neat later. :-)

Best wishes and enjoy the Tea Party.

Reply all
Reply to author
0 new messages