Contributions to the theory of practical quantified Boolean formula solving
From MaRDI portal
Publication:4899301
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
- Moving definition variables in quantified Boolean formulas
- Subsumption-linear Q-resolution for QBF theorem proving
- Clause/Term resolution and learning in the evaluation of quantified Boolean formulas
- Proof complexity of symbolic QBF reasoning
- Theory and Applications of Satisfiability Testing
- Resolution for quantified monosigned formulae
- Lifting QBF resolution calculi to DQBF
- Theory and Applications of Satisfiability Testing
- scientific article; zbMATH DE number 1884351 (Why is no real title available?)
- Hardness Characterisations and Size-width Lower Bounds for QBF Resolution
- Quantified maximum satisfiability
- Automata, Languages and Programming
- A self-adaptive multi-engine solver for quantified Boolean formulas
- scientific article; zbMATH DE number 1979551 (Why is no real title available?)
- A game characterisation of tree-like Q-resolution size
- Hardness and optimality in QBF proof systems modulo NP
- Theory and Applications of Satisfiability Testing
- Extended Failed-Literal Preprocessing for Quantified Boolean Formulas
- On Stronger Calculi for QBFs
- Classes of hard formulas for QBF resolution
- scientific article; zbMATH DE number 1950260 (Why is no real title available?)
- Expansion-based QBF solving versus Q-resolution
- Theory and Applications of Satisfiability Testing
- scientific article; zbMATH DE number 1903342 (Why is no real title available?)
- Characterising tree-like Frege proofs for QBF
- From (Quantified) Boolean Formulae to Answer Set Programming
- Relating size and width in variants of Q-resolution
- Lower bound techniques for QBF proof systems
- Efficient reduction of nondeterministic automata with application to language inclusion testing
- QELL: QBF reasoning with extended clause learning and levelized SAT solving
- An effective algorithm for the futile questioning problem
- Binary Clause Reasoning in QBF
- Q-resolution with generalized axioms
- scientific article; zbMATH DE number 5139165 (Why is no real title available?)
- Principles and Practice of Constraint Programming – CP 2004
- scientific article; zbMATH DE number 2090309 (Why is no real title available?)
- Recent Findings in Boolean Techniques
- Partial implicit unfolding in the Davis-Putnam procedure for quantified Boolean formulae
- On quantifying literals in Boolean logic and its applications to explainable AI
- Solving QBF with counterexample guided refinement
- Long-distance Q-resolution with dependency schemes
- Resolution on quantified generalized clause-sets
- A Splitting Algorithm Based on Soft Constraints for the Computation of Truth Degree in Quantitative Logic
- A game characterisation of tree-like Q-resolution size
- scientific article; zbMATH DE number 7029312 (Why is no real title available?)
- scientific article; zbMATH DE number 7278086 (Why is no real title available?)
- Clause elimination for SAT and QSAT
- A non-prenex, non-clausal QBF solver with game-state learning
- Failed literal detection for QBF
- Size, cost and capacity: a semantic technique for hard random QBFs
- scientific article; zbMATH DE number 2119676 (Why is no real title available?)
- The QBF Gallery: behind the scenes
- scientific article; zbMATH DE number 2090051 (Why is no real title available?)
- Feasible interpolation for QBF resolution calculi
- A polyhedral projection procedure for Q2SAT
- An Operator for Removal of Subsumed Clauses
- Understanding cutting planes for QBFs
- Reinterpreting dependency schemes: soundness meets incompleteness in DQBF
- Software for quantifier elimination in propositional logic
- Never trust your solver: certification for SAT and QBF
- True crafted formula families for benchmarking quantified satisfiability solvers
- Computing smallest MUSes of quantified Boolean formulas
- On Q-resolution and CDCL QBF solving
- QBFFam: a tool for generating QBF families from proof complexity
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)
