QBFFam: a tool for generating QBF families from proof complexity

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

Luca Pulina, Ankit Shukla, Olaf Beyersdorff, Martina Seidl

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

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

Related Items (3)

QBFFam ⋮ True crafted formula families for benchmarking quantified satisfiability solvers ⋮ Classes of hard formulas for QBF resolution

Uses Software

• DepQBF
• CNFgen
• RAReQS

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Solving QBF with counterexample guided refinement
• On the power of clause-learning SAT solvers as resolution engines
• The intractability of resolution
• Symmetries of quantified Boolean formulas
• Short proofs for some symmetric quantified Boolean formulas
• Resolution for 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)
• Expansion-based QBF solving versus Q-resolution
• DepQBF 6.0: a search-based QBF solver beyond traditional QCDCL
• Unified QBF certification and its applications
• A simple proof of QBF hardness
• On Q-Resolution and CDCL QBF Solving
• Long-Distance Resolution: Proof Generation and Strategy Extraction in Search-Based QBF Solving
• QBF Resolution Systems and Their Proof Complexities
• New Results on the Phase Transition for Random Quantified Boolean Formulas
• Contributions to the Theory of Practical Quantified Boolean Formula Solving
• Automated Testing and Debugging of SAT and QBF Solvers
• Dynamic QBF Dependencies in Reduction and Expansion
• CAQE and QuAbS: Abstraction Based QBF Solvers
• Hardness Characterisations and Size-Width Lower Bounds for QBF Resolution
• New Resolution-Based QBF Calculi and Their Proof Complexity

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