temp.txt

Dear Tomas and all SAT Competition organizers,

Thanks for the email and thank you for organizing the competition. It was fun and I understand how complicated it must have been to organize it, especially in these really weird times. So, thanks so much for doing it!


Unfortunately, reading through the slides, I believe the solvers by Shaowei Cai and Xindi Zhang, and all CaDiCaL solvers not authored by Armin Biere, violated the following rule: "By a portfolio SAT solver we mean a combination of two or more (core) SAT solvers developed by different groups of authors. Participation of portfolio SAT solvers is not allowed".

The solver submitted by Shaowei Cai and Xindi Zhang violated this rule -- the authors of Maple* solver were not present in their submission, yet it's a portfolio solver by your definition. See our discussion with Marijn, previously. According to that discussion, an exception is only possible in case both solvers' authors are added to the author list. Note that I tried to add a local search solver to CMS (yalsat) and was asked to add Armin Biere to the list of authors -- similarly: walksat (Bart Selman+Henry Kautz), CCAnr (Shaowei Cai). Hence SLS+CDCL needs both sets of authors. I believe CDCL+SLS is the same, therefore must add all authors. But the submission is missing the Maple* authors. Hence, by this rule, these solvers would need to be disqualified.

Similarly, all solvers that are CaDiCaL based but not authored by Armin Biere also seem to fit this category. The CaDiCaL solver is a hybrid solver, both CDCL and SLS developed by Armin Biere. The CDCL part of the solver was changed, hence the CDCL part is now authored by those who submitted the solver. However, the SLS part of the solver was untouched, in a separate file, clearly marked as authored by Armin Biere, exactly the way I added yalsat, walksat and CCAnr. Due to the requirement that hybrid solvers of different authorships are considered portfolio, the authors of both must be represented in the authors list. However, Armin Biere is not listed as an author, hence by this rule, these solvers would also need to be disqualified.

I believe the above two reasonings, and how obviously harmful they are to building community should be an alarm bell: this policy needs refinement/fixing. I understand (and encourage) that portfolio solvers are not welcome. And I also understand that it is encouraged that researchers create their own solver. But this policy is hurting the community, and making it hard to build on each other's work. Instead of disqualifying the above solvers, I would like to have it acknowledged that this policy, as it is currently formulated, is not commensurate with the goals of (1) encouraging people to collaborate hence build community (since it's hurting collaboration between groups of researchers to reuse each others' code) and (2) encouraging people to build their own solvers (since it's hurting me the most, one of the few who actually build their own solver). I believe now it is the best time to fix this policy, as for next year, we'll have many more solvers wanting to add an SLS component to their current CDCL component.


I again thank you for organizing the competition -- I know it's a lot of (thankless) work, and I am sure you get a few emails like this one. I understand that you are trying to do what you believe is best for the community. I am just trying to highlight that there is an issue here that I believe needs to be addressed. I also understand that it's not easily addressed, but I am certain we can find a way forward to fix it, and in case you would like to, I am happy to help in doing so.

Thanks again for organizing the competition. It was really enjoyable! Please send the medals to:

Mate Soos
Lehmbruckstrasse 11
10245 Berlin
Germany

Thanks again, and looking forward to SAT Comp'2021 with hopefully a more refined rule set,

Mate