DepQBF
From MaRDI portal
Cited in
(84)- QuBE++
- QBFFam
- QRATPre+
- GANAK
- Relating size and width in variants of Q-resolution
- A little blocked literal goes a long way
- \({\textsf{QRAT}}^{+}\): generalizing QRAT by a more powerful QBF redundancy property
- sQueezeBF
- Quaffle
- Skolem functions for DQBF
- A formal methods approach to predicting new features of the eukaryotic vesicle traffic system
- 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
- QBFFam: a tool for generating QBF families from proof complexity
- Lower bounds for QCDCL via formula gauge
- Hardness and optimality in QBF proof systems modulo NP
- Proof complexity of symbolic QBF reasoning
- Advanced algorithms for abstract dialectical frameworks based on complexity analysis of subclasses and SAT solving
- Solving dependency quantified Boolean formulas using quantifier localization
- Bloqqer
- Nenofex
- QUBOS
- QBFLIB
- HeerHugo
- Combining resolution-path dependencies with dependency learning
- Knowledge representation analysis of graph mining
- The 2016 and 2017 QBF solvers evaluations (QBFEVAL'16 and QBFEVAL'17)
- Reinterpreting dependency schemes: soundness meets incompleteness in DQBF
- CirQit2
- QUBE
- Expansion-based QBF solving versus Q-resolution
- QMiraXT
- Solution validation and extraction for QBF preprocessing
- Conformant planning as a case study of incremental QBF solving
- DepQBF 6.0: a search-based QBF solver beyond traditional QCDCL
- Solving QBF with counterexample guided refinement
- Strong (D)QBF dependency schemes via tautology-free resolution paths
- Positional games and QBF: the corrective encoding
- Computing smallest MUSes of quantified Boolean formulas
- Incremental determinization
- On Q-resolution and CDCL QBF solving
- 2QBF: challenges and solutions
- HordeQBF: a modular and massively parallel QBF solver
- Off the Trail: Re-examining the CDCL Algorithm
- Solving QBF with counterexample guided refinement
- Coprocessor
- Incremental QBF solving by DepQBF
- Failed literal detection for QBF
- HordeQBF
- MPIDepQBF
- \(\mathsf{MPIDepQBF}\): towards parallel QBF solving without knowledge sharing
- A unified proof system for QBF preprocessing
- GRAPPA
- Lpopt
- CNFgen
- DIAMOND
- Bounded synthesis for Petri games
- Preprocessing for DQBF
- Incrementally Computing Minimal Unsatisfiable Cores of QBFs via a Clause Group Solver API
- QELL: QBF reasoning with extended clause learning and levelized SAT solving
- QBFEVAL
- CAQE
- AIGSolve
- Quantor
- semprop
- HQSpre
- selp
- Integrating dependency schemes in search-based QBF solvers
- Solving Advanced Argumentation Problems with Answer Set Programming
- Planning with Incomplete Information in Quantified Answer Set Programming
- Blocked clause elimination for QBF
- Backdoors to normality for disjunctive logic programs
- On propositional QBF expansions and Q-resolution
- Recovering and utilizing partial duality in QBF
- Efficient Clause Learning for Quantified Boolean Formulas via QBF Pseudo Unit Propagation
- eclingo
- sKizzo
- RAReQS
- Aeon
- QESTO
- dCAQE
- GhostQ
- Logic-based ontology comparison and module extraction, with an application to DL-Lite
- Proof complexity of modal resolution
This page was built for software: DepQBF
