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 NP-complete 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 low-level reasoning with only Boolean variables, whereas most problem domains have higher-level information and data types such as integers, reals, finite precision (e.g., 32-bit) integers (i.e., bit-vectors), 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 first-order theories. The idea is to apply higher-level 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 fixed-size bit-vectors. Given an SMT formula, Beaver first performs word-level simplifications and then bit-blasts it to solve using any SAT solver. Several engineering techniques are behind its efficiency:
-
1) efficient constant/constraint propagation using event-driven approach;
2) several word-level rewrite rules; and
3) efficient bit-blasting to SAT, by first converting to and-inverter-graph (AIG) representation and using Boolean simplification techniques of ABC logic synthesis system [2].