QBFFam: a tool for generating QBF families from proof complexity

DOI10.1007/978-3-030-80223-3_3OpenAlexW3184306867MaRDI QIDQ2118282FDOQ2118282

Authors: Olaf Beyersdorff, Luca Pulina, Martina Seidl, Ankit Shukla 

Publication date: 22 March 2022

Full work available at URL: https://doi.org/10.1007/978-3-030-80223-3_3

zbMATH Keywords

benchmarkingquantified Boolean formulasformula generator

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Analysis of algorithms and problem complexity (68Q25) Computational aspects of satisfiability (68R07)

Cites Work

• Resolution for quantified Boolean formulas
• Expansion-based QBF solving versus Q-resolution
• Unified QBF certification and its applications
• Solving QBF with counterexample guided refinement
• Contributions to the theory of practical quantified Boolean formula solving
• Title not available (Why is that?)
• Long-distance resolution: proof generation and strategy extraction in search-based QBF solving
• QBF Resolution Systems and Their Proof Complexities
• Automated testing and debugging of SAT and QBF solvers
• The intractability of resolution
• On the power of clause-learning SAT solvers as resolution engines
• DepQBF 6.0: a search-based QBF solver beyond traditional QCDCL
• Title not available (Why is that?)
• Hardness Characterisations and Size-Width Lower Bounds for QBF Resolution
• New resolution-based QBF calculi and their proof complexity
• Feasible interpolation for QBF resolution calculi
• Symmetries of quantified Boolean formulas
• A simple proof of QBF hardness
• On Q-resolution and CDCL QBF solving
• Dynamic QBF dependencies in reduction and expansion
• Short proofs for some symmetric quantified Boolean formulas
• Building strategies into QBF proofs
• Proof complexity of QBF symmetry recomputation
• The 2016 and 2017 QBF solvers evaluations (QBFEVAL'16 and QBFEVAL'17)
• New Results on the Phase Transition for Random Quantified Boolean Formulas
• CAQE and QuAbS: Abstraction Based QBF Solvers

Cited In (4)

• Classes of hard formulas for QBF resolution
• \({\textsf{QRAT}}^{+}\): generalizing QRAT by a more powerful QBF redundancy property
• QBFFam
• True crafted formula families for benchmarking quantified satisfiability solvers

Uses Software

• DepQBF
• CNFgen
• RAReQS

This page was built for publication: QBFFam: a tool for generating QBF families from proof complexity

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