SAT & SMT

June 8, 2022 at 8:51 pm

Basic Concepts

Proof Checker

Solver

Verified/Certified Solver

VeriT

  • Can be used with external checkers, e.g. SMTCoq

versat: A Verified Modern SAT Solver

  • No code, not usable
  • Dependent Type; Guru-lang

Papers

SMT Solver Funzzing

Formal(ly Verified) SAT/SMT Solver

Proof Checking

Also see the related articles.

Other Resources