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



Mathias, congratulations, this is just amazing! Formal verification triumphs over hackery - let there be light! And thanks to Peter for all of his refinement tools down to LLVM.

Tobias

On 28/07/2021 12:50, Peter Lammich wrote:
The SAT solver ISASAT <https://m-fleury.github.io/isasat/isasat.html> by Mathias Fleury has won the EDA Fixed CNF Encoding Race <https://www.eda-ai.org/>, 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 <https://www21.in.tum.de/~lammich/isabelle_llvm/>.

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


Attachment: smime.p7s
Description: S/MIME Cryptographic Signature



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