The QBF Gallery 2023
Simone Heisinger, Luca Pulina, Martina Seidl
TL;DR
The QBF Gallery 2023 reports on the state of the art in solving quantified Boolean formulas, presenting new benchmarks, solver evaluations, and future research directions.
Contribution
It introduces a consolidated benchmark set and provides a comprehensive analysis of solver performance in the QBF community.
Findings
New benchmark set combining well-evaluated formulas and submitted instances
Comparative analysis of solver performance and capabilities
Discussion on future directions for QBF research and benchmarking
Abstract
The QBF Gallery 2023, the last QBF evaluation event, continues the tradition to survey and document the state of the art in solving quantified Boolean formulas (QBFs). It provides a detailed overview by collecting newly developed solvers and formulas as benchmarks. This report documents the solvers and formulas submitted by the community and introduces a new, consolidated benchmark set that combines well-evaluated formulas with the submitted instances. The resulting formula set is made publicly available. With this benchmark set, we conduct a comparative analysis of the submitted solvers and publicly available solvers, assessing their performance and current capabilities. In addition, we report on the present status of the QBF Gallery and discuss ideas and directions for future editions to further support research and benchmarking within the QBF community.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.