Susmit Kumar Jha and Rhishikesh Shrikant Limaye and Sanjit A. Seshia

EECS Department, University of California, Berkeley

Technical Report No. UCB/EECS-2009-95

June 30, 2009

http://www2.eecs.berkeley.edu/Pubs/TechRpts/2009/EECS-2009-95.pdf

We present the key ideas in the design and implementation of Beaver, an SMT solver for quantifierfree finite-precision bit-vector logic (QF BV). Beaver uses an eager approach, encoding the original SMT problem into a Boolean satisfiability (SAT) problem using a series of word-level and bit-level transformations. In this paper, we describe the most effective transformations, such as propagating constants and equalities at the word-level, and using and-inverter graph rewriting techniques at the bit-level. We highlight the implementation details of these transformations that distinguishes Beaver from other solvers. We present an experimental evaluation and analysis of the effectiveness of Beaver’s techniques on both hardware and software benchmarks with a selection of back-end SAT solvers.

Beaver is an open-source tool implemented in Ocaml, usable with any back-end SAT engine, and has a well-documented extensible code base that can be used to experiment with new algorithms and techniques.

---

BibTeX citation:

@techreport{Jha:EECS-2009-95,
    Author= {Jha, Susmit Kumar and Limaye, Rhishikesh Shrikant and Seshia, Sanjit A.},
    Title= {Beaver: Engineering an Efficient SMT Solver for Bit-Vector Arithmetic},
    Year= {2009},
    Month= {Jun},
    Url= {http://www2.eecs.berkeley.edu/Pubs/TechRpts/2009/EECS-2009-95.html},
    Number= {UCB/EECS-2009-95},
    Abstract= {We present the key ideas in the design and implementation of Beaver, an SMT solver for quantifierfree
finite-precision bit-vector logic (QF BV). Beaver uses an eager approach, encoding the original
SMT problem into a Boolean satisfiability (SAT) problem using a series of word-level and bit-level
transformations. In this paper, we describe the most effective transformations, such as propagating constants
and equalities at the word-level, and using and-inverter graph rewriting techniques at the bit-level.
We highlight the implementation details of these transformations that distinguishes Beaver from other
solvers. We present an experimental evaluation and analysis of the effectiveness of Beaver’s techniques
on both hardware and software benchmarks with a selection of back-end SAT solvers.

Beaver is an open-source tool implemented in Ocaml, usable with any back-end SAT engine, and
has a well-documented extensible code base that can be used to experiment with new algorithms and
techniques.},
}

EndNote citation:

%0 Report
%A Jha, Susmit Kumar 
%A Limaye, Rhishikesh Shrikant 
%A Seshia, Sanjit A. 
%T Beaver: Engineering an Efficient SMT Solver for Bit-Vector Arithmetic
%I EECS Department, University of California, Berkeley
%D 2009
%8 June 30
%@ UCB/EECS-2009-95
%U http://www2.eecs.berkeley.edu/Pubs/TechRpts/2009/EECS-2009-95.html
%F Jha:EECS-2009-95