The QBF Gallery: behind the scenes
From MaRDI portal
Publication:286397
DOI10.1016/J.ARTINT.2016.04.002zbMATH Open1357.68209arXiv1508.01045OpenAlexW2194993457MaRDI QIDQ286397FDOQ286397
Allen Van Gelder, Martina Seidl, Florian Lonsing
Publication date: 20 May 2016
Published in: Artificial Intelligence (Search for Journal in Brave)
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.
Full work available at URL: https://arxiv.org/abs/1508.01045
Cites Work
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- Title not available (Why is that?)
- sQueezeBF: An Effective Preprocessor for QBFs Based on Equivalence Reasoning
- Blocked Clause Elimination for QBF
- Resolution for quantified Boolean formulas
- Expansion-based QBF solving versus Q-resolution
- Unified QBF certification and its applications
- Solving QBF with Counterexample Guided Refinement
- On Unification of QBF Resolution-Based Calculi
- Failed Literal Detection for QBF
- Contributions to the Theory of Practical Quantified Boolean Formula Solving
- A Non-prenex, Non-clausal QBF Solver with Game-State Learning
- On Propositional QBF Expansions and Q-Resolution
- Experiments with Reduction Finding
- Long-Distance Resolution: Proof Generation and Strategy Extraction in Search-Based QBF Solving
- QBF Resolution Systems and Their Proof Complexities
- A Unified Proof System for QBF Preprocessing
- Recovering and Utilizing Partial Duality in QBF
- Extended Failed-Literal Preprocessing for Quantified Boolean Formulas
- Compressing BMC encodings with QBF
- SAT-Based Synthesis Methods for Safety Specs
- Careful Ranking of Multiple Solvers with Timeouts and Ties
- Finding Reductions Automatically
- Encoding Techniques, Craig Interpolants and Bounded Model Checking for Incomplete Designs
- The Seventh QBF Solvers Evaluation (QBFEVAL’10)
- Efficient Clause Learning for Quantified Boolean Formulas via QBF Pseudo Unit Propagation
Cited In (6)
- Solving QBF with counterexample guided refinement
- Q-Resolution with Generalized Axioms
- 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
Uses Software
Recommendations
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)
