SAT Competition 2023 This year, once again, I submitted IsaSAT to the SAT Competition 2023 (the source code is as always available). According to the results, I did not finish last. However, compared to other solvers, I am trailing in the unsatisfiable instances. I believe that this is due to the fact that I still do not have bounded variable elimination. In the past, I assumed that vivification was also very important, but its importance is now less clear after Daniela and I attempted to examine it more precisely for POS'23 on the SAT solver CaDiCaL. …

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