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