Resources for SAT/SMT Solvers

Some of the problems in the homework assignments will require the use of SAT/SMT solvers.

There are many SAT/SMT solvers that are available for free download. They are not all at the same stage of development, nor do they all support the same functionalities, and some are not maintained. One of the most advanced, and possibly best supported currently, is Z3. In the assignments we will ask you to use Z3 exclusively; this webpage is meant to ease your way into using Z3.

• Instructions for installing Z3 on your computer are in a tutorial posted under General Resources on Piazza (search for Z3_SMT_LIB.tutorial.txt).
     
• The website SMT-LIB -- whose name is an acronym for Satisfiability Modulo Theories Library -- the goals of which include:
  • the development of common input and output languages for SAT/SMT solvers,
  • the maintenance of a large library of benchmarks for SAT/SMT solvers.
       
• If you are a Python programmer,
  • you will find a Python API (Application Progam Interface) for SAT/SMT solvers at the website pySMT. pySMT does not promote, and does not depend on, any single SAT/SMT solver. However, if you want to carry out some solving, you need to have at least one SAT/SMT solver installed -- for CS 511 this semester, it has to be Z3.
    For plenty of additional information, inspect the GitHub pages for pySMT.
  • you will find a useful tutorial for a Python API that is committed to Z3 at the website Z3 API in Python.
  
     
• If you are an OCaml programmer,
  • Instructions for installing the OCaml API for Z3 on a Unix/Linux computer are in a tutorial posted under General Resources on Piazza (search for Ocaml_install_notes.txt).
  • you will find an API (Application Progam Interface) called Why3 for SMT solvers (as well as interactive proof assistants such as Coq and Isabelle) at the website Why3 and plenty of information for how to use Why3.
  
     
• If you are an aficionado of automated and semi-automated tools for software engineering, check out the website rise4fun from Microsoft Research, which includes many of the links elsewhere on this webpage.