Satisfiability modulo theories (SMT) can be seen an an extended form of propositional satisfiability, where propositions are either simple boolean propositions or constraints in a specific theory. MathSAT is a DPLL-based decision procedure for the SMT problem for various theories, including those of Equality and Uninterpreted Function (EUF), Difference Logics (DL), Linear Arithmetic over the Reals (LA(R)) and Linear Arithmetic over the Integers (LA(Z)).

MathSAT is based on the approach of integrating a state-of-the-art SAT solver with a hierarchy of dedicated solvers for the different theories, and implements several optimization techniques. MathSat pioneers a lazy and layered approach, where propositional reasoning is tightly integrated with solvers of increasing expressive power, in such a way that more expensive layers are called less frequently.

MathSAT has been applied in different real-world application domains, ranging from formal verification of infinite state systems (e.g. timed and hybrid systems) to planning with resources, equivalence checking and model checking of RTL hardware designs.