Abstract
In both the hardware and the software domains, non-canonical circuit-based state set representations have recently been the subject of intensive investigations. One of the limiting factors of these representations has been the difficulty to control their size during key operations. For example, existentially and universally quantifying a variable implies doubling the circuit size in the worst case.
In this paper, we present a probabilistic approach to keep under control the size of circuit-based representations when manipulating them. Every time a formula is becoming too cumbersome, we estimate it instead of building the exact result. The nature of the estimate, i.e., under- or over-approximation, depends on the problem that is being computed. The key idea of this process is to boost the expressiveness of the formula, delivering a dense representation, i.e., a formula compact in size but more expressive for the given verification problem.
Experimental results show decisive reductions in terms of circuit size, and an increase in terms of density, i.e., the ratio between the cardinality of the on-set of a formula and the size of its representation. We applied the strategy to Bounded Model Checkingm, and circuit-based backward Unbounded Model Checking. We present experimental results from applying the approach to hard-to-solve verification instances. We observed speedups of more than one order of magnitude in some cases.