Programming Z3

Explore the intricacies of Satisfiability Modulo Theories (SMT) and programming Z3 in this 51-minute lecture by Nikolaj Björner from Microsoft Research. Delve into the foundations of SMT, including its relationship with SAT solvers and theory solvers. Learn about the CDCL(T) algorithm, its implementation as inference rules, and the process of combining theories. Discover practical applications through examples such as a solver for Unicode characters and solving arithmetic problems. Gain insights into advanced topics like consequential SMT, cores, and correction sets. Examine the main theory interfaces and explore solver technologies beyond CDCL(T). This comprehensive talk, part of the Satisfiability: Theory, Practice, and Beyond Boot Camp at the Simons Institute, provides a thorough overview of current developments and active areas in the field of SMT solving.