SAT Competition 2024 There is not much to tell for the release for this year of the SAT Competition 2024. This year, I finished last, exactly as expected. However, I am very close to the second-to-last on SAT benchmarks. My main performance problem seems to be UNSAT problems, which I blame on missing preprocessing. I intended to implement variable elimination based on the model reconstruction implemented in Katharina Wagner’s Master’s thesis in Isabelle. I actually started to implement it, but, as usual, once I went to proofs, things became more complicated. But it is interesting. …

IsaSAT is one of the few verified SAT solvers (and to my knowledge the only one that is currently maintained). It is verified in Isabelle using the Isabelle Refinement Framework by synthesizing code. See the presentation for more details.

As part of my PhD thesis, I developed a framework to formalize SAT solving. I still continue to expand it. The general organization is given by the following graph: . If you want to have a look at the sources, look at the IsaFoL repository (this is the latest bleeding age version, so it is sometimes broken) and the Isabelle-generated HTML documentation (look at the “IsaFoL” version at the bottom to know the corresponding git ID). …

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. …