Here the release of my projects that I manage myself (so unlike my changes to, e.g., CaDiCaL).

IsaSAT

2021: EDA Challenge

This the first official release of the IsaSAT in LLVM IR. See the sources and the system description submitted at the EDA Challenge for a list of changes compared to IsaSAT in Standard ML.

The main difference compared to the Standard ML version developped in my PhD is that the Isabelle theorem is now incomplete (this was implicit earlier in the sense that it is a limit of the compiler, not a limit of the program) and that the new version is much faster.

IsaSAT in Standard ML

This is the last version of our IsaSAT sources in Standard ML: Sources. The compiler MLton is the only compiler we tried that offers reasonnable performance.

Pastèque

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

The release is also available here with the unverified checker PACheck.