Techniques and Standards for Evaluating ATP Techniques and Implementations

[Geoff Sutcliffe]

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]

Let me add to this discussion the links I provided in the Zoom chat:

https://github.com/danielleberre/satpractitionermanisfesto

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

http://www.pragmaticsofsat.org/2020/

which actually was captured on Video

https://github.com/danielleberre/satpractitionermanisfesto

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]

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

https://zenodo.org/record/4500928

[Michael Rawson]

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