[isabelle] Announcement: Verified SAT Solver ISASAT wins EDA Fixed CNF Encoding Race

The SAT solver ISASAT by Mathias Fleury has won the EDA Fixed CNF Encoding Race, a competition affiliated with this years SAT conference.

Except for parsing of the input and printing of results, full functional correctness of this solver is verified, down to LLVM intermediate code, 
using Isabelle/LLVM.

As far as I know, this was the only formally verified solver in the field!

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.