Symbolic AI is an approach to Artificial Intelligence that uses deductive reasoning to produce exact and explainable results to well-defined problems, compared to sub-symbolic methods (e.g. machine learning, deep NNs, LLMs, etc.), which use statistical learning to tackle a wide variety of tasks (possibly vaguely defined) to produce plausible answers (which can however be incorrect and that are usually not explainable). Integration between symbolic and sub-symbolic methods is a hot topic in AI.
SMT solvers are tools that can be used to reason about and rigorously solve different kinds of problems, involving arithmetic, arrays, bit vectors, etc. They are used in industrial applications for several tasks, such as program verification, planning, testing, etc.
In this lesson, we introduce z3, an efficient and user-friendly SMT solver developed by Microsoft. We will compare it to both user-written algorithms and LLMs on a simple task such as solving a Sudoku. We will also see how to use z3 to solve the Die Hard jug riddle (a model checking problem).
Finally, we will give a few exercises to experiment with the tool.
Install z3 Python APIs through pip:
pip3 install z3-solver
- C. Barrett, R. Sebastiani, S. Seshia, C. Tinelli: Satisfiability Modulo Theories, 2018
- L. de Moura, N. Bjørner: Z3: An Efficient SMT Solver, 2008
- A. Biere, D. Kröning: SAT-Based Model Checking, 2018
- A. Biere, M. Heule, H. Van Maaren, T. Walsh: Handbook of Satisfiability, 2021
- J. Aldrich: Lecture Notes on Satisfiability Modulo Theories, 2019
- M. Fredrikson: Lecture Notes on Bounded Model Checking, 2022