Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Announcement: Verified SAT Solver ISASAT wins ...


view this post on Zulip Email Gateway (Jul 28 2021 at 10:51):

From: Peter Lammich <lammich@in.tum.de>
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!

view this post on Zulip Email Gateway (Jul 28 2021 at 11:04):

From: Tobias Nipkow <nipkow@in.tum.de>
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
smime.p7s

view this post on Zulip Email Gateway (Jul 28 2021 at 21:12):

From: Andrei Popescu <andrei.h.popescu@gmail.com>
On Wed, Jul 28, 2021 at 12:07 PM Tobias Nipkow <nipkow@in.tum.de> wrote:

Mathias, congratulations, this is just amazing! Formal verification triumphs
over hackery - let there be light!

Indeed. :-) Congrats, Mathias and Peter, awesome achievement!

Best wishes,
Andrei

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!


Last updated: Dec 05 2021 at 22:18 UTC