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

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.
978-3-030-80222-6
978-3-030-80223-3
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].
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: http://hdl.handle.net/11388/276459
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 0
  • ???jsp.display-item.citation.isi??? 0
social impact