Clause/Term resolution and learning in the evaluation of quantified Boolean formulas
From MaRDI portal
Recommendations
- Contributions to the theory of practical quantified Boolean formula solving
- Efficient Clause Learning for Quantified Boolean Formulas via QBF Pseudo Unit Propagation
- QELL: QBF reasoning with extended clause learning and levelized SAT solving
- An algorithm to evaluate quantified Boolean formulae and its experimental evaluation
- Dependency learning for QBF
Cited in
(38)- Non-binary quantified CSP: Algorithms and modelling
- Clause trees: A tool for understanding and implementing resolution in automated reasoning
- Building strategies into QBF proofs
- Dual proof generation for quantified Boolean formulas with a BDD-based solver
- Lower bounds for QCDCL via formula gauge
- Characterising tree-like Frege proofs for QBF
- The 2016 and 2017 QBF solvers evaluations (QBFEVAL'16 and QBFEVAL'17)
- Expansion-based QBF solving versus Q-resolution
- Solving quantified constraint satisfaction problems
- Conformant planning as a case study of incremental QBF solving
- Long-distance Q-resolution with dependency schemes
- Henkin quantifiers and Boolean formulae: a certification perspective of DQBF
- Unified QBF certification and its applications
- On Q-resolution and CDCL QBF solving
- Q-resolution with generalized axioms
- 2QBF: challenges and solutions
- Long distance Q-resolution with dependency schemes
- HordeQBF: a modular and massively parallel QBF solver
- The QBF Gallery: behind the scenes
- Abstraction-based algorithm for 2QBF
- Failed literal detection for QBF
- Incrementally Computing Minimal Unsatisfiable Cores of QBFs via a Clause Group Solver API
- QELL: QBF reasoning with extended clause learning and levelized SAT solving
- A Unified Framework for Certificate and Compilation for QBF
- Learning to integrate deduction and search in reasoning about quantified Boolean formulas
- scientific article; zbMATH DE number 1950260 (Why is no real title available?)
- ALLQBF solving by computational learning
- Contributions to the theory of practical quantified Boolean formula solving
- A non-prenex, non-clausal QBF solver with game-state learning
- Efficient Clause Learning for Quantified Boolean Formulas via QBF Pseudo Unit Propagation
- Pool Resolution and Its Relation to Regular Resolution and DPLL with Clause Learning
- Binary Clause Reasoning in QBF
- Clause-Learning Algorithms with Many Restarts and Bounded-Width Resolution
- Lower bounds for QCDCL via formula gauge
- Understanding the Relative Strength of QBF CDCL Solvers and QBF Resolution
- Logic-based ontology comparison and module extraction, with an application to DL-Lite
- Reasoning with propositional logic: from SAT solvers to knowledge compilation
- Soundness of \(\mathcal{Q}\)-resolution with dependency schemes
This page was built for publication: Clause/Term resolution and learning in the evaluation of quantified Boolean formulas
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3624018)
