Preprocessing for DQBF
From MaRDI portal
Publication:3453223
DOI10.1007/978-3-319-24318-4_13zbMath1471.68264OpenAlexW2185821556MaRDI QIDQ3453223
Ralf Wimmer, Bernd Becker, Karina Gitina, Jennifer Nist, Christoph Scholl
Publication date: 20 November 2015
Published in: Lecture Notes in Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-319-24318-4_13
Related Items (6)
Preprocessing for DQBF ⋮ Solving dependency quantified Boolean formulas using quantifier localization ⋮ Building strategies into QBF proofs ⋮ Dependency Schemes for DQBF ⋮ Lifting QBF Resolution Calculi to DQBF ⋮ The (D)QBF Preprocessor HQSpre – Underlying Theory and Its Implementation1
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Thread-parallel integrated test pattern generator utilizing satisfiability analysis
- Backdoor sets of quantified Boolean formulas
- Toward leaner binary-clause reasoning in a satisfiability solver
- Henkin quantifiers and Boolean formulae: a certification perspective of DQBF
- Computing Resolution-Path Dependencies in Linear Time ,
- Incremental QBF Solving by DepQBF
- Efficient CNF Simplification Based on Binary Implication Graphs
- Variable Independence and Resolution Paths for Quantified Boolean Formulas
- Fast DQBF Refutation
- Preprocessing for DQBF
- Blocked Clause Elimination
- Algorithms for computing backbones of propositional formulae
- sQueezeBF: An Effective Preprocessor for QBFs Based on Equivalence Reasoning
- Clause Elimination Procedures for CNF Formulas
- Efficiently Representing Existential Dependency Sets for Expansion-based QBF Solvers
- Blocked Clause Elimination for QBF
- Variable Dependencies of Quantified CSPs
- Depth-First Search and Linear Graph Algorithms
- Theory and Applications of Satisfiability Testing
- Theory and Applications of Satisfiability Testing
- Theory and Applications of Satisfiability Testing
- Dependency Quantified Horn Formulas: Models and Complexity
- Applications of SAT Solvers to Cryptanalysis of Hash Functions
- Lower bounds for multiplayer noncooperative games of incomplete information
This page was built for publication: Preprocessing for DQBF
