Abstract: Over the last few years, much progress has been made in the theory and practice of solving quantified Boolean formulas (QBF). Novel solvers have been presented that either successfully enhance established techniques or implement novel solving paradigms. Powerful preprocessors have been realized that tune the encoding of a formula to make it easier to solve. Frameworks for certification and solution extraction emerged that allow for a detailed interpretation of a QBF solver's results, and new types of QBF encodings were presented for various application problems. To capture these developments the QBF Gallery was established in 2013. The QBF Gallery aims at providing a forum to assess QBF tools and to collect new, expressive benchmarks that allow for documenting the status quo and that indicate promising research directions. These benchmarks became the basis for the experiments conducted in the context of the QBF Gallery 2013 and follow-up evaluations. In this paper, we report on the setup of the QBF Gallery. To this end, we conducted numerous experiments which allowed us not only to assess the quality of the tools, but also the quality of the benchmarks.
Recommendations
Cites work
- scientific article; zbMATH DE number 5542982 (Why is no real title available?)
- scientific article; zbMATH DE number 1950260 (Why is no real title available?)
- scientific article; zbMATH DE number 5493266 (Why is no real title available?)
- A non-prenex, non-clausal QBF solver with game-state learning
- A unified proof system for QBF preprocessing
- Blocked clause elimination for QBF
- Careful ranking of multiple solvers with timeouts and ties
- Clause/Term resolution and learning in the evaluation of quantified Boolean formulas
- Compressing BMC encodings with QBF
- Contributions to the theory of practical quantified Boolean formula solving
- Efficient Clause Learning for Quantified Boolean Formulas via QBF Pseudo Unit Propagation
- Encoding techniques, Craig interpolants and bounded model checking for incomplete designs
- Expansion-based QBF solving versus Q-resolution
- Experiments with reduction finding
- Extended Failed-Literal Preprocessing for Quantified Boolean Formulas
- Failed literal detection for QBF
- Finding Reductions Automatically
- Long-distance resolution: proof generation and strategy extraction in search-based QBF solving
- On Unification of QBF Resolution-Based Calculi
- On propositional QBF expansions and Q-resolution
- Planning as quantified Boolean formula
- Proof complexity of resolution-based QBF calculi
- QBF Resolution Systems and Their Proof Complexities
- Recovering and utilizing partial duality in QBF
- Resolution for quantified Boolean formulas
- SAT-Based Synthesis Methods for Safety Specs
- Solving QBF with counterexample guided refinement
- The seventh QBF solvers evaluation (QBFEVAL'10)
- Unified QBF certification and its applications
- sQueezeBF: an effective preprocessor for QBFs based on equivalence reasoning
Cited in
(6)- Q-resolution with generalized axioms
- Solving QBF with counterexample guided refinement
- The 2016 and 2017 QBF solvers evaluations (QBFEVAL'16 and QBFEVAL'17)
- On the complexity of inconsistency measurement
- Solution validation and extraction for QBF preprocessing
- Never trust your solver: certification for SAT and QBF
This page was built for publication: The QBF Gallery: behind the scenes
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q286397)
