True Crafted Formula Families for Benchmarking Quantified Satisfiability Solvers.

As the application of quantified Boolean formulas (QBF) continues to expand in various scientific and industrial domains, the development of efficient QBF solvers and their underlying proving strategies is of growing importance. To understand and to compare different solving approaches, techniques of proof complexity are applied. To this end, formula families have been crafted that exhibit certain properties of proof systems. These formulas are valuable to test and compare specific solver implementations. Traditionally, the focus is on false formulas, in this work we extend the formula generator QBFFam to produce true formulas based on two popular formula families from proof complexity.