Tags:Isabelle, program verification, SAT solving and synthesis
Abstract:
IsaSAT is the most advanced verified SAT solver, but it does not feature inprocessing (simplify and strengthen clauses). In order to improve performance, we enriched the base calculus to not only do CDCL but also inprocess clauses. We also replaced the target of our code synthesis by Isabelle/LLVM. With these improvements, we can solve 4 times more SAT competition 2022 problems than the original IsaSAT version, and 4.5 times more problems than any other verified SAT solver we are aware of. Additionally, our changes significantly reduce the trusted code base of our verification.
A More Pragmatic CDCL for IsaSAT and Targetting LLVM