At a high-level, the architecture of many SMT solvers is well known. It is the combination of a SAT solver and one or more decision procedures called theory solvers. But how to e ectively implement such a combination is rarely discussed in the literature. This talk will focus on implementation issues. We will discuss the practical integration of CDCL-based SAT solvers and theory solvers. We will present data structures and algorithms employed by the Yices SMT solver, and examine preprocessing and formula simpli cation, which have a signi cant impact on a solver's performance.

Yices is developed and distributed by SRI International. It is free for non-commercial use. Source and binaries are available at http://yices.csl.sri.com.