QBFFam: a tool for generating QBF families from proof complexity
From MaRDI portal
Publication:2118282
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
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 (2)
Uses Software
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
