MathSAT logo

MathSAT 4

An SMT solver for Formal Verification
Home | Documentation | Download | Publications | Performance | Links | The MathSAT Team | MathSAT 3.x (Old)
NOTICE: MathSAT 4 is no longer being developed! Consider upgrading to MathSAT 5 instead.

Introduction

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 4 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 4 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 4 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 4 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.

MathSAT 4 is a from-scratch reimplementation of MathSAT 3.x, offering improved performance and several new features which are particularly useful in the context of Formal Verification, like generation of models, unsatisfiable cores, and interpolants.

MathSAT 4 is a joint project of DISI-University of Trento and FBK-IRST.

FBKUniTN