Lemma and model caching in decision procedures for quantified Boolean formulas
From MaRDI portal
Recommendations
- A satisfiability procedure for quantified Boolean formulae
- Clause/Term resolution and learning in the evaluation of quantified Boolean formulas
- QUBOS: Deciding quantified Boolean logic using propositional satisfiability solvers
- Contributions to the theory of practical quantified Boolean formula solving
- Formula Caching in DPLL
Cited in
(19)- A solver for QBFs in negation normal form
- On deciding subsumption problems
- Two SAT solvers for solving quantified Boolean formulas with an arbitrary number of quantifier alternations
- From QBFs to \textsf{MALL} and back via focussing
- The 2016 and 2017 QBF solvers evaluations (QBFEVAL'16 and QBFEVAL'17)
- Conformant planning as a case study of incremental QBF solving
- Computational methods for database repair by signed formulae
- Solving QBF with counterexample guided refinement
- Q-resolution with generalized axioms
- HordeQBF: a modular and massively parallel QBF solver
- The QBF Gallery: behind the scenes
- Validating QBF Validity in HOL4
- Incrementally Computing Minimal Unsatisfiable Cores of QBFs via a Clause Group Solver API
- A Compact Representation for Syntactic Dependencies in QBFs
- semprop
- OuterCount: a first-level solution-counter for quantified Boolean formulas
- Never trust your solver: certification for SAT and QBF
- Subsumption-linear Q-resolution for QBF theorem proving
- The complexity of pure literal elimination
This page was built for publication: Lemma and model caching in decision procedures for quantified Boolean formulas
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4412858)
