Contributions to the theory of practical quantified Boolean formula solving
From MaRDI portal
Publication:4899301
DOI10.1007/978-3-642-33558-7_47zbMATH Open1390.68585OpenAlexW1851471023MaRDI QIDQ4899301FDOQ4899301
Authors: 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
Recommendations
- Efficient Clause Learning for Quantified Boolean Formulas via QBF Pseudo Unit Propagation
- Clause/Term resolution and learning in the evaluation of quantified Boolean formulas
- QELL: QBF reasoning with extended clause learning and levelized SAT solving
- Clause elimination for SAT and QSAT
- scientific article; zbMATH DE number 2119676
Cited In (66)
- Towards Uniform Certification in QBF
- QBF merge resolution is powerful but unnatural
- Subsumption-linear Q-resolution for QBF theorem proving
- Moving definition variables in quantified Boolean formulas
- Title not available (Why is that?)
- Solving QBF with counterexample guided refinement
- The QBF Gallery: behind the scenes
- Binary Clause Reasoning in QBF
- A polyhedral projection procedure for Q2SAT
- Quantified maximum satisfiability
- Title not available (Why is that?)
- Hardness and optimality in QBF proof systems modulo NP
- Recent Findings in Boolean Techniques
- Efficient reduction of nondeterministic automata with application to language inclusion testing
- Title not available (Why is that?)
- Hardness Characterisations and Size-width Lower Bounds for QBF Resolution
- A self-adaptive multi-engine solver for quantified Boolean formulas
- Title not available (Why is that?)
- A non-prenex, non-clausal QBF solver with game-state learning
- Failed literal detection for QBF
- Theory and Applications of Satisfiability Testing
- Resolution for quantified monosigned formulae
- Lifting QBF resolution calculi to DQBF
- Classes of hard formulas for QBF resolution
- A game characterisation of tree-like Q-resolution size
- Theory and Applications of Satisfiability Testing
- Relating size and width in variants of Q-resolution
- Principles and Practice of Constraint Programming – CP 2004
- Reinterpreting dependency schemes: soundness meets incompleteness in DQBF
- Theory and Applications of Satisfiability Testing
- Expansion-based QBF solving versus Q-resolution
- Resolution on quantified generalized clause-sets
- Understanding cutting planes for QBFs
- On Q-resolution and CDCL QBF solving
- Clause/Term resolution and learning in the evaluation of quantified Boolean formulas
- Automata, Languages and Programming
- A Splitting Algorithm Based on Soft Constraints for the Computation of Truth Degree in Quantitative Logic
- Clause elimination for SAT and QSAT
- Title not available (Why is that?)
- Proof complexity of symbolic QBF reasoning
- Title not available (Why is that?)
- Characterising tree-like Frege proofs for QBF
- QELL: QBF reasoning with extended clause learning and levelized SAT solving
- Title not available (Why is that?)
- An Operator for Removal of Subsumed Clauses
- A game characterisation of tree-like Q-resolution size
- Size, cost and capacity: a semantic technique for hard random QBFs
- Feasible interpolation for QBF resolution calculi
- Software for quantifier elimination in propositional logic
- On Stronger Calculi for QBFs
- From (Quantified) Boolean Formulae to Answer Set Programming
- Lower bound techniques for QBF proof systems
- Partial implicit unfolding in the Davis-Putnam procedure for quantified Boolean formulae
- Extended Failed-Literal Preprocessing for Quantified Boolean Formulas
- Title not available (Why is that?)
- Theory and Applications of Satisfiability Testing
- Computing smallest MUSes of quantified Boolean formulas
- Long-distance Q-resolution with dependency schemes
- Title not available (Why is that?)
- Title not available (Why is that?)
- Never trust your solver: certification for SAT and QBF
- True crafted formula families for benchmarking quantified satisfiability solvers
- QBFFam: a tool for generating QBF families from proof complexity
- An effective algorithm for the futile questioning problem
- On quantifying literals in Boolean logic and its applications to explainable AI
- Q-resolution with generalized axioms
This page was built for publication: Contributions to the theory of practical quantified Boolean formula solving
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4899301)
