QBFFam: A Tool for Generating QBF Families from Proof Complexity

We present QBFFam, a tool for the generation of formula families originating from the field of proof complexity. Such formula families are used to investigate the strength of proof systems and to show how they relate to each other in terms of simulations and separations. Furthermore, these proof systems underlie the reasoning power of QBF solvers. With our tool, it is possible to generate informative and scalable benchmarks that help to analyse the behavior of solvers. As we will see in this paper, runtime behavior predicted by proof complexity is indeed reflected by recent solver implementations.