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.GitHub.
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.
Automated Testing and Debugging of SAT and QBF Solvers, SAT 2010, Edinburgh, Scotland, UK.
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.