# SAT and SMT

[https://en.wikipedia.org/wiki/Satisfiability](https://en.wikipedia.org/wiki/Satisfiability)

`SAT` [https://en.wikipedia.org/wiki/Boolean\_satisfiability\_problem](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](https://en.wikipedia.org/wiki/Satisfiability_modulo_theories)

`SAT/SMT Tutorials and Summer Schools` [https://github.com/Z3Prover/z3/wiki/Slides](https://github.com/Z3Prover/z3/wiki/Slides)

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

`Z3Prover` [https://github.com/Z3Prover/z3](https://github.com/Z3Prover/z3)

`Z3Prover Documentation` [https://github.com/Z3Prover/z3/wiki/Documentation](https://github.com/Z3Prover/z3/wiki/Documentation) [https://github.com/Z3Prover/z3/wiki/Slides](https://github.com/Z3Prover/z3/wiki/Slides)

`Z3 - online guide` [https://rise4fun.com/z3/tutorial/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](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](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.
