Human Folly about “SMT”

index

Src (smt.st):
TeX source code to Yurichev's #ebook about #SAT/#SMT.
on 02024-06-23
SAT SMT by example (smt.st):
#PDF #ebook “#SAT/#SMT by Example” by Dennis Yurichev, 671 pp. “The author of these lines is no expert in SAT/SMT, by any means. This is not a book, rather a student’s notes.” A very extensive set of examples; the English isn’t perfect but generally is comprehensible. #toread
on 02024-06-23
Programmingz3 (z3prover.github.io):
the main #documentation on how to use #Z3, including for #optimization #SAT #SMT
on 02024-06-23
Z3%20Tutorial (colab.research.google.com):
#Z3 #tutorial #documentation that covers things like validating numerical approximation algorithms and training neural networks with it #SAT #SMT
on 02024-06-23
Guide examples (ericpony.github.io):
Leonardo de Moura’s #tutorial #documentation #introduction to #Z3 in Python. It starts out focusing on things like integers, real numbers, and arbitrary precision, but then moves on to bitvectors, bit-twiddling hacks, sudoku, N-queens, and package management. #SAT #SMT
on 02024-06-23
SMTInterpol (ultimate.informatik.uni-freiburg.de):
"SMTInterpol" #SMT solver. #formal-methods #SAT
on 02024-06-16
SMTInterpol (smt-comp.github.io):
#SMT-COMP #PDF #paper about #SMTInterpol, a DPLL(T)/CDCL #SMT solver in Java licensed under LGPLv3. #toread #formal-methods #SAT
on 02024-06-16
(cvc5.github.io):
"CVC5" (Cooperating Validity Checker 5), based on #Minisat, written in C++, and licensed under a 3-clause BSD license, is kind of the top #SMT solver according to the #SMT-COMP results. You can hook it up to #ABC, #CryptoMiniSat, #libpoly, #GMP, #CaDiCal, #symfpu, #CLN (the Class Library for Numbers), and #GLPK. #toread #formal-methods #SAT
on 02024-06-16
CVC5 (smt-comp.github.io):
#SMT-COMP #PDF #paper about the #CVC5 CDCL(T) #SMT solver, the top winner in many categories, licensed under a BSD license. #SAT #formal-methods #toread
on 02024-06-16
iProver (smt-comp.github.io):
#SMT-COMP #PDF #paper about #iProver. #toread #formal-methods #SMT #SAT
on 02024-06-16
iProver (gitlab.com):
#SMT-COMP winner "iProver" is a first-order theorem prover written in OCaml licensed under GPL2+. It wraps #Z3 and #Minisat #SAT solvers. #formal-methods #SMT
on 02024-06-16
(vprover.github.io):
#SMT-COMP winner "Vampire" is under a 3-clause BSD license. #SMT #SAT #formal-methods
on 02024-06-16
Vampire (smt-comp.github.io):
#SMT-COMP #PDF #paper about #Vampire, a first-order theorem prover. #toread #formal-methods #SMT #SAT
on 02024-06-16
(yices.csl.sri.com):
#SMT-COMP winner "Yices2" #SMT #SAT #formal-methods
on 02024-06-16
Yices2 (smt-comp.github.io):
#PDF #SMT-COMP paper about the #Yices2 CDCL(T) #SMT solver, which supports three different #SAT solver backends: CaDiCaL, CryptoMiniSat, and Kissat. #formal-methods
on 02024-06-16
(bitwuzla.github.io):
The "Bitwuzla" #SMT solver, one of the 02023 #SMT-COMP winners, is also under an MIT license. #formal-methods
on 02024-06-16
Bitwuzla (smt-comp.github.io):
#PDF #paper about the #Bitwuzla #SMT solver at #SMT-COMP, a C++ rewrite of a fork of Boolector. #SAT #toread #formal-methods
on 02024-06-16
Z3Pp (github.com):
The "Z3++" #SMT solver, based on #Z3, one of the 02023 #SMT-COMP winners, under basically an MIT license #formal-methods
on 02024-06-16
Z3%2B%2B (smt-comp.github.io):
#PDF #paper about the #Z3++ #SMT solver, which is based on #Z3. #SAT #toread #formal-methods
on 02024-06-16
OpenSMT (smt-comp.github.io):
#PDF #paper about the #OpenSMT T-DPLL #SMT solver, which is based on MiniSAT. #SAT #toread #formal-methods
on 02024-06-16
OpenSMT (github.com):
The "OpenSMT" #SMT (#SAT plus theories) solver, one of the 02023 #SMT-COMP winners, under basically an MIT license #formal-methods
on 02024-06-16
Results (smt-comp.github.io):
#SMT and #SAT competition "SMT-COMP" has many divisions now. #formal-methods
on 02024-06-16