Contributions to the Theory of Practical Quantified Boolean Formula Solving

DOI10.1007/978-3-642-33558-7_47zbMath1390.68585OpenAlexW1851471023MaRDI QIDQ4899301

Allen van Gelder

Publication date: 8 January 2013

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-642-33558-7_47

Mathematics Subject Classification ID

Related Items (29)

Quantified maximum satisfiability ⋮ Hardness Characterisations and Size-width Lower Bounds for QBF Resolution ⋮ The QBF Gallery: behind the scenes ⋮ Feasible Interpolation for QBF Resolution Calculi ⋮ Relating size and width in variants of Q-resolution ⋮ Lower Bound Techniques for QBF Proof Systems ⋮ Long-distance Q-resolution with dependency schemes ⋮ Unnamed Item ⋮ Never trust your solver: certification for SAT and QBF ⋮ True crafted formula families for benchmarking quantified satisfiability solvers ⋮ A game characterisation of tree-like Q-resolution size ⋮ Towards Uniform Certification in QBF ⋮ Subsumption-linear Q-resolution for QBF theorem proving ⋮ Characterising tree-like Frege proofs for QBF ⋮ Understanding cutting planes for QBFs ⋮ A Game Characterisation of Tree-like Q-resolution Size ⋮ On Q-Resolution and CDCL QBF Solving ⋮ On Stronger Calculi for QBFs ⋮ Q-Resolution with Generalized Axioms ⋮ Lifting QBF Resolution Calculi to DQBF ⋮ Unnamed Item ⋮ Reinterpreting dependency schemes: soundness meets incompleteness in DQBF ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Expansion-based QBF solving versus Q-resolution ⋮ Solving QBF with counterexample guided refinement ⋮ QBFFam: a tool for generating QBF families from proof complexity ⋮ Hardness and optimality in QBF proof systems modulo NP ⋮ Proof complexity of symbolic QBF reasoning

This page was built for publication: Contributions to the Theory of Practical Quantified Boolean Formula Solving