UTFacultiesEEMCSDisciplines & departmentsFormal Methods and ToolsNewsFormally Verified SAT-Solver IsaSAT wins EDA Challenge

Formally Verified SAT-Solver IsaSAT wins EDA Challenge

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.