Resolve and expand
From MaRDI portal
Recommendations
- Two SAT solvers for solving quantified Boolean formulas with an arbitrary number of quantifier alternations
- On expansion and resolution in CEGAR based QBF solving
- Expansion-based QBF solving on tree decompositions
- QELL: QBF reasoning with extended clause learning and levelized SAT solving
- Short proofs in QBF expansion
Cited in
(48)- A self-adaptive multi-engine solver for quantified Boolean formulas
- A solver for QBFs in negation normal form
- Backdoor sets of quantified Boolean formulas
- Dual proof generation for quantified Boolean formulas with a BDD-based solver
- Two SAT solvers for solving quantified Boolean formulas with an arbitrary number of quantifier alternations
- Proof complexity of symbolic QBF reasoning
- On expansion and resolution in CEGAR based QBF solving
- Ranking function synthesis for bit-vector relations
- Solution validation and extraction for QBF preprocessing
- Solving quantified constraint satisfaction problems
- Conformant planning as a case study of incremental QBF solving
- Efficiently solving quantified bit-vector formulas
- Predicate Elimination for Preprocessing in First-Order Theorem Proving
- Incremental determinization
- Q-resolution with generalized axioms
- Dependency schemes for DQBF
- Compressing BMC encodings with QBF
- Partial implicit unfolding in the Davis-Putnam procedure for quantified Boolean formulae
- Failed literal detection for QBF
- Preprocessing for DQBF
- QELL: QBF reasoning with extended clause learning and levelized SAT solving
- Nenofex: Expanding NNF for QBF Solving
- A Unified Framework for Certificate and Compilation for QBF
- Bounded Universal Expansion for Preprocessing QBF
- A Compact Representation for Syntactic Dependencies in QBFs
- Beyond CNF: A Circuit-Based QBF Solver
- Learning to integrate deduction and search in reasoning about quantified Boolean formulas
- Quantor
- Symbolic algorithmic verification of intransitive generalized noninterference
- QUBOS: Deciding quantified Boolean logic using propositional satisfiability solvers
- Incremental preprocessing methods for use in BMC
- Quantifier elimination by dependency sequents
- The (D)QBF preprocessor HQSpre -- underlying theory and its implementation
- CAQE and QuAbS: Abstraction Based QBF Solvers
- Efficiently representing existential dependency sets for expansion-based QBF solvers
- Blocked clause elimination for QBF
- Expansion-based QBF solving on tree decompositions
- Backdoors to normality for disjunctive logic programs
- On propositional QBF expansions and Q-resolution
- Evaluating QBFs via symbolic Skolemization
- Quantifier trees for QBFs
- SAT-Inspired Eliminations for Superposition
- Mining definitions in Kissat with Kittens
- Never trust your solver: certification for SAT and QBF
- SAT solving for variants of first-order subsumption
- Quantified constraint handling rules
- Symbolic techniques in satisfiability solving
- Models and quantifier elimination for quantified Horn formulas
This page was built for publication: Resolve and expand
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5714773)
