Crafted True Formulas for Benchmarking QBF Solvers

Due to the constantly growing field of applications of quantified Boolean formulas (QBF) in science and industries, the development of QBF solvers and their underlying solution strategies is becoming more and more important. In order to be able to compare the available solvers with each other, there are crafted uniform formulas that are used as benchmarks. Usually in the literature only false formulas are considered, which are grouped into formula families, give as default the solution unsatisfiable. We develop novel formula families that are true. Furthermore, quantifiers of formulas are restructured to check whether a speedup is possible. These modifications are summarised and compared on different solvers based on different proof systems. In addition to the executed benchmarks, formal proofs of some formulas with Q-resolution and ∀ Exp+Res proof systems are included.