Techniques behind SMT solvers

Abstract

SMT problems form an extensive collection of satisfiability problems. Determining the satisfiability of a Boolean expression lies at the basis of this set and forms the backbone of the P versus NP problem. We study several existing algorithms that solve satisfiability. Another common SMT problem are systems of linear integer inequalities. We look at a few ways these can be solved. Finally, we show how Liquid Haskell uses an SMT solver to verify refinement types.