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.
QBFFam: A Tool for Generating QBF Families from Proof Complexity / Beyersdorff, O.; Pulina, L.; Seidl, M.; Shukla, A.. - 12831:(2021), pp. 21-29. (Intervento presentato al convegno 24th International Conference on Theory and Applications of Satisfiability Testing, SAT 2021 tenutosi a esp nel 2021) [10.1007/978-3-030-80223-3_3].
QBFFam: A Tool for Generating QBF Families from Proof Complexity
Pulina L.;
2021-01-01
Abstract
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.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
