2009 Research Summary
Satisfiability Modulo Theories (SMT)
View Current Project Information
Rhishikesh Shrikant Limaye, Sanjit A. Seshia and Susmit Jha
MICRO
The problem of satisfiability (SAT) is defined as checking whether a given Boolean formula can be satisfied. Although it is a classic NPcomplete problem, in practice, SAT solving techniques have improved dramatically over the last decade. Several fast SAT solvers, capable of handling significantly large problem instances, are easily available today. Still, SAT solvers perform rather lowlevel reasoning with only Boolean variables, whereas most problem domains have higherlevel information and data types such as integers, reals, finite precision (e.g., 32bit) integers (i.e., bitvectors), arrays, strings, and lists.
The problem of Satisfiability Modulo Theories (SMT) concerns satisfiability of a formula made up of not just Boolean variables and operators, but also the ones from other firstorder theories. The idea is to apply higherlevel reasoning, instead of or before handing it down to SAT. SMT solvers are the core components of tools in several areas, including the formal verification of hardware, program analysis, software test generation, and security.
Beaver [1] is an efficient SMT solver for the theory of fixedsize bitvectors. Given an SMT formula, Beaver first performs wordlevel simplifications and then bitblasts it to solve using any SAT solver. Several engineering techniques are behind its efficiency:

1) efficient constant/constraint propagation using eventdriven approach;
2) several wordlevel rewrite rules; and
3) efficient bitblasting to SAT, by first converting to andinvertergraph (AIG) representation and using Boolean simplification techniques of ABC logic synthesis system [2].