QBFFam: a tool for generating QBF families from proof complexity

DOI10.1007/978-3-030-80223-3_3MaRDI QIDQ2118282zbMATH OpenOpenAlexFDO

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

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

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

Describes a project that uses

Uses Software

• RAReQS
• CNFgen
• DepQBF

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)