The (D)QBF Preprocessor HQSpre – Underlying Theory and Its Implementation1
From MaRDI portal
Publication:5015602
DOI10.3233/SAT190115zbMath1484.68225OpenAlexW2995789353MaRDI QIDQ5015602
Christoph Scholl, Bernd Becker, Ralf Wimmer
Publication date: 9 December 2021
Published in: Journal on Satisfiability, Boolean Modeling and Computation (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.3233/sat190115
Related Items
Solving dependency quantified Boolean formulas using quantifier localization, On preprocessing for weighted MaxSAT, Certified DQBF solving by definition extraction, DQBDD: an efficient BDD-based DQBF solver
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Quantifier reordering for QBF
- Incremental preprocessing methods for use in BMC
- Soundness of \(\mathcal{Q}\)-resolution with dependency schemes
- Efficient SAT-based bounded model checking for software verification
- Thread-parallel integrated test pattern generator utilizing satisfiability analysis
- Backdoor sets of quantified Boolean formulas
- A structure-preserving clause form translation
- Complexity results for classes of quantificational formulas
- An algorithm to evaluate quantified Boolean formulae and its experimental evaluation
- Dependency learning for QBF
- A resolution-style proof system for DQBF
- From DQBF to QBF by dependency elimination
- Toward leaner binary-clause reasoning in a satisfiability solver
- Resolution for quantified Boolean formulas
- On a generalization of extended resolution
- Skolem functions for DQBF
- Clausal abstraction for DQBF
- DepQBF 6.0: a search-based QBF solver beyond traditional QCDCL
- Henkin quantifiers and Boolean formulae: a certification perspective of DQBF
- Dependency Schemes for DQBF
- Computing Resolution-Path Dependencies in Linear Time ,
- Solving QBF with Counterexample Guided Refinement
- SAT-Based Synthesis Methods for Safety Specs
- Clause Elimination for SAT and QSAT
- Efficient CNF Simplification Based on Binary Implication Graphs
- Variable Independence and Resolution Paths for Quantified Boolean Formulas
- Fast DQBF Refutation
- Preprocessing for DQBF
- iProver – An Instantiation-Based Theorem Prover for First-Order Logic (System Description)
- Blocked Clause Elimination
- Bounded Universal Expansion for Preprocessing QBF
- GRASP: a search algorithm for propositional satisfiability
- Algorithms for computing backbones of propositional formulae
- bv2epr: A Tool for Polynomially Translating Quantifier-Free Bit-Vector Formulas into EPR
- 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
- Theory and Applications of Satisfiability Testing
- Variable Dependencies of Quantified CSPs
- Depth-First Search and Linear Graph Algorithms
- The complexity of theorem-proving procedures
- 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
- Bounded model checking using satisfiability solving
- Lower bounds for multiplayer noncooperative games of incomplete information
