swMATH9578MaRDI QIDQ21559FDOQ21559
Author name not available (Why is that?)
Official website: http://fmv.jku.at/bloqqer/
Cited In (58)
- Local redundancy in SAT: generalizations of blocked clauses
- Solving QBF with counterexample guided refinement
- Solving QBF with counterexample guided refinement
- The QBF Gallery: behind the scenes
- Conformant planning as a case study of incremental QBF solving
- Algorithms for computing minimal equivalent subformulas
- The 2016 and 2017 QBF solvers evaluations (QBFEVAL'16 and QBFEVAL'17)
- Advanced algorithms for abstract dialectical frameworks based on complexity analysis of subclasses and SAT solving
- Planning with Incomplete Information in Quantified Answer Set Programming
- RAReQS
- Quantifier reordering for QBF
- QESTO
- A game characterisation of tree-like Q-resolution size
- Recovering and utilizing partial duality in QBF
- A unified proof system for QBF preprocessing
- QuBE++
- NiVER
- sQueezeBF
- Quaffle
- Nenofex
- DepQBF
- QBFLIB
- QUBOS
- CirQit2
- QUBE
- QMiraXT
- Coprocessor
- Incremental determinization
- Super-blocked clauses
- GRAPPA
- HordeQBF
- MPIDepQBF
- QBFEVAL
- AIGSolve
- CAQE
- Quantor
- HQSpre
- semprop
- QELL: QBF reasoning with extended clause learning and levelized SAT solving
- 2QBF: challenges and solutions
- Truth assignments as conditional autarkies
- cnf2aig
- sKizzo
- Preprocessing for DQBF
- Solution validation and extraction for QBF preprocessing
- On QBF Proofs and Preprocessing
- Two SAT solvers for solving quantified Boolean formulas with an arbitrary number of quantifier alternations
- Encodings of bounded synthesis
- PReLearn
- QRATPre+
- Extended Failed-Literal Preprocessing for Quantified Boolean Formulas
- Long-distance Q-resolution with dependency schemes
- SAT-Inspired Eliminations for Superposition
- Enhancing search-based QBF solving by dynamic blocked clause elimination
- HordeQBF: a modular and massively parallel QBF solver
- Incrementally Computing Minimal Unsatisfiable Cores of QBFs via a Clause Group Solver API
- Q-resolution with generalized axioms
- Long distance Q-resolution with dependency schemes
This page was built for software: Bloqqer
