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

DOI10.1016/J.ARTINT.2019.04.002MaRDI QIDQ2321317zbMATH OpenOpenAlexWikidataFDO

Authors Luca Pulina, Martina Seidl

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

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

Recommendations

• The seventh QBF solvers evaluation (QBFEVAL'10)
• Report of the third QBF solvers evaluation
• Theory and Applications of Satisfiability Testing
• Theory and Applications of Satisfiability Testing
• Twelve years of QBF evaluations: QSAT is PSPACE-hard and it shows

Cites work

• scientific article; zbMATH DE number 1950260 (Why is no real title available?)
• A non-prenex, non-clausal QBF solver with game-state learning
• A self-adaptive multi-engine solver for quantified Boolean formulas
• Abstraction-based algorithm for 2QBF
• Automated testing and debugging of SAT and QBF solvers
• Blocked clause elimination for QBF
• Clause/Term resolution and learning in the evaluation of quantified Boolean formulas
• DepQBF 6.0: a search-based QBF solver beyond traditional QCDCL
• Dependency learning for QBF
• Enhancing search-based QBF solving by dynamic blocked clause elimination
• Evaluating and certifying QBFs: a comparison of state-of-the-art tools
• Failed literal detection for QBF
• HordeQBF: a modular and massively parallel QBF solver
• HordeSat: a massively parallel portfolio SAT solver
• Incremental determinization
• Inst-Gen -- a modular approach to instantiation-based automated reasoning
• Non-prenex QBF solving using abstraction
• On the computational cost of disjunctive logic programming: Propositional case
• QELL: QBF reasoning with extended clause learning and levelized SAT solving
• SAT race 2015
• Silhouettes: a graphical aid to the interpretation and validation of cluster analysis
• Solving QBF with counterexample guided refinement
• Solving QBF with counterexample guided refinement
• Soundness of \(\mathcal{Q}\)-resolution with dependency schemes
• The QBF Gallery: behind the scenes
• The seventh QBF solvers evaluation (QBFEVAL'10)
• Theory and Applications of Satisfiability Testing
• Twelve years of QBF evaluations: QSAT is PSPACE-hard and it shows
• \(\mathsf{MPIDepQBF}\): towards parallel QBF solving without knowledge sharing
• sQueezeBF: an effective preprocessor for QBFs based on equivalence reasoning

Cited in

(19)

• Certified DQBF solving by definition extraction
• Lower bounds for QCDCL via formula gauge
• DQBDD: an efficient BDD-based DQBF solver
• Theory and Applications of Satisfiability Testing
• Hardness Characterisations and Size-width Lower Bounds for QBF Resolution
• DepQBF 6.0: a search-based QBF solver beyond traditional QCDCL
• Understanding the Relative Strength of QBF CDCL Solvers and QBF Resolution
• The seventh QBF solvers evaluation (QBFEVAL'10)
• Report of the third QBF solvers evaluation
• Theory and Applications of Satisfiability Testing
• Lower bounds for QCDCL via formula gauge
• Twelve years of QBF evaluations: QSAT is PSPACE-hard and it shows
• A simple proof of QBF hardness
• CAQE and QuAbS: Abstraction Based QBF Solvers
• OuterCount: a first-level solution-counter for quantified Boolean formulas
• Common equivalence and size of forgetting from Horn formulae
• Transforming quantified Boolean formulas using biclique covers
• QBFFam: a tool for generating QBF families from proof complexity
• Never trust your solver: certification for SAT and QBF

Describes a project that uses

Uses Software

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

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2321317)