While I don’t understand much algebra, I know Isabelle and implemented a checker in Isabelle/HOL. I used the Refinement Framework and Sepref to generated code in Standard ML. The code is mostly functional (except for the hashmap that is synthesized automatically by Sepref – no need to understand and know anything about it!). How does Pastèque work? I started with an abstract calculus that models the rules of the proofs system. Then I make the calculus more concrete, e.g., with lists to represent polynomials. Finally, I make everything executable. …

Pastèque 2 Pastèque 2 is available on the IsaFoL repository and the HTML generation can be seen too. The source code can be found here. Pastèque 1 Pastèque 1 is available with the Isabelle formalization on the Archive of Formal Proofs, where it is maintained and kept up-to-date. The release is also available here.

2024 Robin Coutelier, Mathias Fleury and Laura Kovács, Lazy Reimplication in Chronological Backtracking SAT 2024 preprint @InProceedings{coutelier_et_al:LIPIcs.SAT.2024.9, author = {Coutelier, Robin and Fleury, Mathias and Kov\'{a}cs, Laura}, title = {{Lazy Reimplication in Chronological Backtracking}}, booktitle = {27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)}, pages = {9:1--9:19}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-334-8}, ISSN = {1868-8969}, year = {2024}, volume = {305}, editor = {Chakraborty, Supratik and Jiang, Jie-Hong Roland}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2024.9}, URN = {urn:nbn:de:0030-drops-205313}, doi = {10.4230/LIPIcs.SAT.2024.9}, annote = {Keywords: Chronological Backtracking, CDCL, Invariants, Watcher Lists} } …

This is the detailed story of my Tweet about the used flag. Database Reduction Some background first. CDCL solvers learns clauses. Actually they generate way too many clauses to keep all of them. So you have to remove them. Actually many of them. This happens during so-called reductions. This comes from the theory of CDCL. There are two way to keep completeness: either delay restarts more-and-more or keep more-and-more clauses. But this does not tell you which clauses you have to keep during reductions. …

Artifacts Reviewing I have consistently felt unease about our approach to examining artifacts. Although I have personally reviewed numerous artifacts, I believe that, as a community, we are mistaken in our methods. Weird Errors and Artifact Problems The objective of artifact creation is straightforward: to enable the reproducibility of results by allowing the same code to be run again in the future. This can be achieved by packaging all necessary components in a repository, such as Zenodo, ensuring that everything is self-contained and does not rely on external internet connections. Indeed, this approach seems quite appealing. …