SMT solver

[Google Scholar] [Wikipedia]

Notes: Z3 solver, CVC4 solver, SMT-LIB format, SAT solver
Papers: barrett:cade:2000, brummayer:sat:2010, mansur:arxiv:2020, stump:fmsd:2013, barrett:mlf:2015, baldoni:compsurv:2018

todo:

A good summary of SMT from baldoni:compsurv:2018 is

Observe that some problems are more naturally described with languages that are more expressive than the one of boolean formulas with logical connectives. For this reason, satisfiability modulo theories (SMT) generalize the SAT problem with supporting theories to capture formulas involving, for instance, linear arithmetic and operations over arrays. SMT solvers map the atoms in an SMT formula to fresh boolean variables: a SAT decision procedure checks the rewritten formula for satisfiability, and a theory solver checks the model generated by the SAT procedure.
— baldoni:compsurv:2018

[SMT-COMP website] is very significant and probably a good way to find SMT solvers and to select one or two to consider for a new project.

List of major solvers

And Vampire, that is a theorem prover pretending to be an SMT solver? https://vprover.github.io

Testing of SMT solvers

brummayer:sat:2010 and mansur:arxiv:2020 tested SMT solvers and found bugs. There are several proposals such as stump:fmsd:2013 and barrett:mlf:2015 for a proof format that would allow SMT proofs to be checked.

[SMT-COMP website]: https://smt-comp.github.io/

CVC4 solver, Omega library, SAT solver, SMT-LIB format, Z3 theorem prover