Armin Biere, Toni Jussila,
"Compressing BMC Encodings with QBF"
: Proc. 4th Intl. Workshop on Bounded Model Checking (BMC'06), Seattle, USA, Serie Electronic Notes in Theoretical Computer Science (ENTCS), 2006
Original Titel:
Compressing BMC Encodings with QBF
Sprache des Titels:
Englisch
Original Buchtitel:
Proc. 4th Intl. Workshop on Bounded Model Checking (BMC'06), Seattle, USA
Original Kurzfassung:
Symbolic model checking is PSPACE complete. Since QBF is the standard
PSPACE complete problem, it is most natural to encode symbolic model
checking problems as QBF formulas and then use QBF decision procedures
to solve them. We discuss alternative encodings for unbounded and
bounded safety checking into SAT and QBF. One contribution is a linear
encoding of simple path constraints, which usually are necessary to
make $k$-induction complete. Our experimental results show that indeed a
large reduction in the size of the generated formulas can be obtained.
However, current QBF solvers seem not to be able to take advantage of
these compact formulations. Despite these mostly negative results the
availability of these benchmarks will help improve the state of the art
of QBF solvers and make QBF based symbolic model checking a viable
alternative.
Sprache der Kurzfassung:
Englisch
Serie:
Electronic Notes in Theoretical Computer Science (ENTCS)
Forschungs-