Techniques and Standards for Evaluating ATP Techniques and Implementations

14 views
Skip to first unread message

Geoff Sutcliffe

unread,
Jul 16, 2021, 9:43:07 AMJul 16
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.

Cheers,

Geoff

Armin Biere

unread,
Jul 16, 2021, 10:28:29 AMJul 16
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.

Armin

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

unread,
Jul 16, 2021, 10:29:22 AMJul 16
to TPTP World

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

Michael Rawson

unread,
Jul 16, 2021, 1:15:19 PMJul 16
to TPTP World
Hi all,

Thanks for your input and support! I've made https://docs.google.com/document/d/1JjMwksUVaDMTSOIG-9MX525Zk6R_paZ0i98t4kAJrKs/edit?usp=sharing to collect all of your ideas. Go mad, we can make it neat later. :-)

Best wishes and enjoy the Tea Party.

Michael
Reply all
Reply to author
Forward
0 new messages