Construction of efficient BDDs for bounded arithmetic constraints

Abstract

Most symbolic model checkers use BDDs to represent arithmetic constraints over bounded integer variables. The size of such BDDs can be exponential on the number and size (in bits) of the integer variables in the worst case. In this paper we show how to construct linear-sized BDDs for linear integer arithmetic constraints. We present basic constructions for atomic equality and inequality constraints and extend them to handle arbitrary linear arithmetic formulas. We also present three alternative ways of handling out-of-bounds transitions, and discuss multiple bounds on integer variables. We experimentally compare our approach to other BDD-based symbolic model checkers and demonstrate that the algorithms presented in this paper can be used to improve their performance significantly. © Springer-Verlag Berlin Heidelberg 2003.