Robert Brummayer, Armin Biere,
"Effective Bit-Width and Under-Approximation"
: Proc. 12th Intl. Conference on Computer Aided Systems Theory (EUROCAST'09), Lecture Notes in Computer Science (LNCS), Vol. 5717, Seite(n) 304-311, 2-2009
Effective Bit-Width and Under-Approximation
Sprache des Titels:
Proc. 12th Intl. Conference on Computer Aided Systems Theory (EUROCAST'09), Lecture Notes in Computer Science (LNCS)
Recently, it has been proposed to use approximation techniques
in the context of decision procedures for the quantifier-free theory
of fixed-size bit-vectors. We discuss existing and novel variants of underapproximation
techniques. Under-approximations produce smaller models
and may reduce solving time significantly. We propose a new technique
that allows early termination of an under-approximation refinement
loop, although the original formula is unsatisfiable. Moreover, we
show how over-approximation and under-approximation techniques can
be combined. Finally, we evaluate the effectiveness of our approach on
array and bit-vector benchmarks of the SMT library.