The QBF Gallery: behind the scenes

DOI10.1016/j.artint.2016.04.002zbMath1357.68209arXiv1508.01045OpenAlexW2194993457MaRDI QIDQ286397

Martina Seidl, Florian Lonsing, Allen van Gelder

Publication date: 20 May 2016

Published in: Artificial Intelligence (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1508.01045

zbMATH Keywords

quantified Boolean formulaQBF benchmarksQBF competitionQBF gallery

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)

Related Items

Solution validation and extraction for QBF preprocessing, Never trust your solver: certification for SAT and QBF, Q-Resolution with Generalized Axioms, The 2016 and 2017 QBF solvers evaluations (QBFEVAL'16 and QBFEVAL'17), On the complexity of inconsistency measurement, Solving QBF with counterexample guided refinement

Uses Software

• sQueezeBF
• Quaffle
• Bloqqer
• QBFLIB
• ABC
• semprop
• AutoFolio
• RAReQS

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Resolution for quantified Boolean formulas
• Expansion-based QBF solving versus Q-resolution
• Unified QBF certification and its applications
• Extended Failed-Literal Preprocessing for Quantified Boolean Formulas
• Solving QBF with Counterexample Guided Refinement
• Compressing BMC Encodings with QBF
• Long-Distance Resolution: Proof Generation and Strategy Extraction in Search-Based QBF Solving
• On Unification of QBF Resolution-Based Calculi
• SAT-Based Synthesis Methods for Safety Specs
• Failed Literal Detection for QBF
• Careful Ranking of Multiple Solvers with Timeouts and Ties
• QBF Resolution Systems and Their Proof Complexities
• A Unified Proof System for QBF Preprocessing
• Finding Reductions Automatically
• Contributions to the Theory of Practical Quantified Boolean Formula Solving
• sQueezeBF: An Effective Preprocessor for QBFs Based on Equivalence Reasoning
• A Non-prenex, Non-clausal QBF Solver with Game-State Learning
• Encoding Techniques, Craig Interpolants and Bounded Model Checking for Incomplete Designs
• The Seventh QBF Solvers Evaluation (QBFEVAL’10)
• Blocked Clause Elimination for QBF
• On Propositional QBF Expansions and Q-Resolution
• Recovering and Utilizing Partial Duality in QBF
• Efficient Clause Learning for Quantified Boolean Formulas via QBF Pseudo Unit Propagation
• Experiments with Reduction Finding