2020-10-01 13:57:4 (GMT)
Propose papers and vote on them before 15/10 (Thursday in two weeks)
2020-10-01 13:57:58 (GMT)
One SAT paper about proof: »Using Resolution Proofs to Analyse CDCL Solvers« from Janne I. Kokkala and Jakob Nordström
https://link.springer.com/chapter/10.1007/978-3-030-58475-7_25
2020-10-01 14:12:44 (GMT)
Code Trees for E-Matching: »Efficient E-Matching for SMT Solvers« from Leonardo de Moura and Nikolaj Bjørner
http://leodemoura.github.io/files/ematching.pdf
2020-10-01 14:28:25 (GMT)
Mansur, Muhammad Numair, et al. "Detecting Critical Bugs in SMT Solvers Using Blackbox Mutational Fuzzing." arXiv preprint arXiv:2004.05934 (2020).
https://arxiv.org/pdf/2004.05934.pdf
2020-10-02 16:56:20 (GMT)
A slightly left-field suggestion
M. Ganesalingam, W. T. Gowers "A Fully Automatic Theorem Prover with Human-Style Output"
2020-10-02 17:32:39 (GMT)
The most cited JAR paper that year, I believe. Or the most downloaded.
2020-10-03 9:12:17 (GMT)
At least in part, likely to be because of the authors.
2020-10-03 9:49:41 (GMT)
Of course. But also because it's less specialized / technical than most JAR articles, I would guess.
2020-10-07 19:13:3 (GMT)
Kodkod: a relational model finder pdf
it's about SAT encodings, symmetry breaking, etc. that are used to power nitpick in Isabelle.
2020-10-15 12:12:22 (GMT)
We have now three papers with 4 votes. If you have not voted yet, please do so!
2020-10-15 13:16:8 (GMT)
I unvoted on a couple of papers because I won't be able to make it probably.
2020-10-16 18:30:46 (GMT)
Now we have a winner: »Using Resolution Proofs to Analyse CDCL Solvers« from Janne I. Kokkala and Jakob Nordström
and instead of the springer version, let's use http://www.csc.kth.se/~jakobn/research/UsingProofs_CP.pdf
2020-10-16 18:31:59 (GMT)
I cannot edit the title to update it if someone like @Sophie Tourret passes by...