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