SAT and SMT

https://en.wikipedia.org/wiki/Satisfiability

SAT https://en.wikipedia.org/wiki/Boolean_satisfiability_problem In computer science, the Boolean satisfiability problem (sometimes called propositional satisfiability problem and abbreviated as SATISFIABILITY or SAT) is the problem of determining if there exists an interpretation that satisfies a given Boolean formula

Satisfiability modulo theories (SMT) https://en.wikipedia.org/wiki/Satisfiability_modulo_theories

SAT/SMT Tutorials and Summer Schools https://github.com/Z3Prover/z3/wiki/Slides

Fourth Summer School on Formal Techniques http://fm.csl.sri.com/SSFT14/ May 19 - May 23, 2014, Menlo College, Atherton, CA

Z3Prover https://github.com/Z3Prover/z3

Z3Prover Documentation https://github.com/Z3Prover/z3/wiki/Documentation https://github.com/Z3Prover/z3/wiki/Slides

Z3 - online guide https://rise4fun.com/z3/tutorial/guide

SAT solvers Microsoft Research https://www.microsoft.com/en-us/research/people/leonardo/?from=http%3A%2F%2Fresearch.microsoft.com%2Fen-us%2Fum%2Fpeople%2Fleonardo%2Fblog.html

Developing Bug-Free Machine Learning Systems Using Formal Mathematics Microsoft Research https://channel9.msdn.com/Shows/Microsoft-Research/Developing-Bug-Free-Machine-Learning-Systems-Using-Formal-Mathematics

Lean Microsoft Research The Lean theorem prover is an open source dependently typed, interactive theorem prover developed jointly at Microsoft Research and Carnegie Mellon University.