The 2016 and 2017 QBF solvers evaluations (QBFEVAL'16 and QBFEVAL'17)

DOI10.1016/j.artint.2019.04.002zbMath1478.68332OpenAlexW2937448176WikidataQ128067016 ScholiaQ128067016MaRDI QIDQ2321317

Martina Seidl, Luca Pulina

Publication date: 28 August 2019

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

Full work available at URL: https://doi.org/10.1016/j.artint.2019.04.002

zbMATH Keywords

QBF competitionquantified Boolean formulasQBF solving

Mathematics Subject Classification ID

Logic in artificial intelligence (68T27) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (11)

Hardness Characterisations and Size-width Lower Bounds for QBF Resolution ⋮ A simple proof of QBF hardness ⋮ OuterCount: a first-level solution-counter for quantified Boolean formulas ⋮ Never trust your solver: certification for SAT and QBF ⋮ Understanding the Relative Strength of QBF CDCL Solvers and QBF Resolution ⋮ Lower bounds for QCDCL via formula gauge ⋮ CAQE and QuAbS: Abstraction Based QBF Solvers ⋮ QBFFam: a tool for generating QBF families from proof complexity ⋮ Lower bounds for QCDCL via formula gauge ⋮ Certified DQBF solving by definition extraction ⋮ DQBDD: an efficient BDD-based DQBF solver

Uses Software

• Silhouettes
• WEKA
• sQueezeBF
• Quaffle
• StarExec
• Bloqqer
• DepQBF
• HordeSat
• HordeQBF
• MPIDepQBF
• QBFEVAL
• CAQE
• AIGSolve
• semprop
• HQSpre
• RAReQS
• QESTO

Cites Work

• Unnamed Item
• Unnamed Item
• Solving QBF with counterexample guided refinement
• The QBF Gallery: behind the scenes
• SAT race 2015
• Soundness of \(\mathcal{Q}\)-resolution with dependency schemes
• A self-adaptive multi-engine solver for quantified Boolean formulas
• Silhouettes: a graphical aid to the interpretation and validation of cluster analysis
• Dependency learning for QBF
• On the computational cost of disjunctive logic programming: Propositional case
• DepQBF 6.0: a search-based QBF solver beyond traditional QCDCL
• Incremental Determinization
• Non-prenex QBF Solving Using Abstraction
• HordeQBF: A Modular and Massively Parallel QBF Solver
• Solving QBF with Counterexample Guided Refinement
• Abstraction-Based Algorithm for 2QBF
• Failed Literal Detection for QBF
• MPIDepQBF: Towards Parallel QBF Solving without Knowledge Sharing
• Evaluating and certifying QBFs: A comparison of state-of-the-art tools
• HordeSat: A Massively Parallel Portfolio SAT Solver
• QELL: QBF Reasoning with Extended Clause Learning and Levelized SAT Solving
• Enhancing Search-Based QBF Solving by Dynamic Blocked Clause Elimination
• Twelve Years of QBF Evaluations: QSAT Is PSPACE-Hard and It Shows
• Inst-Gen – A Modular Approach to Instantiation-Based Automated Reasoning
• Automated Testing and Debugging of SAT and QBF Solvers
• sQueezeBF: An Effective Preprocessor for QBFs Based on Equivalence Reasoning
• A Non-prenex, Non-clausal QBF Solver with Game-State Learning
• The Seventh QBF Solvers Evaluation (QBFEVAL’10)
• Blocked Clause Elimination for QBF
• Theory and Applications of Satisfiability Testing

This page was built for publication: The 2016 and 2017 QBF solvers evaluations (QBFEVAL'16 and QBFEVAL'17)