Compressing BMC Encodings with QBF

11 years 5 months ago
Compressing BMC Encodings with QBF
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. Key words: Bounded Model Checking, Encoding, QBF, SAT.
Toni Jussila, Armin Biere
Added 13 Dec 2010
Updated 13 Dec 2010
Type Journal
Year 2007
Authors Toni Jussila, Armin Biere
Comments (0)