Wednesday 14 July 2021
The SAT solver IsaSAT by Mathias Fleury has won the fixed CNF encoding race of the 2021 EDA Challenge. All results.
IsaSAT is a formally verified SAT solver, using Peter Lammich's Isabelle LLVM to produce fast verified code.
This is the first time a formally verified solver wins a competition against unverified solvers.