QBFDD

QBFDD is a delta-debugger for quantified boolean formulae (QBF) in QDIMACS format. Given a buggy QBF solver S and a formula F where S fails on F (e.g. crashes, assertion failures,...). QBFDD iteratively removes clauses and literals from F in order to obtain a smaller formula F' while preserving erroneous behaviour of S on F'. The minimization process terminates when no further simplifications are possible. Formula F' can then be used to debug solver S. QBFDD is configurable and offers various minimization strategies. When combined with fuzzing, QBFDD can be effectively used for automated testing of QBF solvers. See also the README file for further information

You might also be interested in QBFuzz, a fuzzer for generating random QBF.

Download

QBFDD is available on GitHub.

Publications

Robert Brummayer, Florian Lonsing, Armin Biere. Automated Testing and Debugging of SAT and QBF Solvers. In Proc. 13th Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT'10), Lecture Notes in Computer Science (LNCS) vol. 6175, pages 44-57, Springer 2010.
[ paper | bibtex ]

Talk Slides

Automated Testing and Debugging of SAT and QBF Solvers, SAT 2010, Edinburgh, Scotland, UK.

License

QBFDD was developed by Aina Niemetz as a bachelor project. It is released under GNU GPLv3. See also file COPYING that is part of the distribution.