Electrical Engineering
      and Computer Sciences

Electrical Engineering and Computer Sciences

COLLEGE OF ENGINEERING

UC Berkeley

   

2010 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 simplications 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, 3) efficient bit-blasting to SAT, by first converting to and-inverter-graph (AIG) representation and using Boolean simplication techniques of ABC logic synthesis system [2].

The future directions of this project are twofold. First, we are extending our solver to handle other theories in order to reason more precisely and efficiently about data and timing. Also, we believe there is scope to bridge the gap between bit-vector SMT problem and Boolean SAT solving techniques, so that bit-vector SMT solvers approach the efficiency of SAT solvers.

[1]
http://uclid.eecs.berkeley.edu/beaver/
[2]
http://www.eecs.berkeley.edu/~alanmi/abc/