The (D)QBF preprocessor HQSpre -- underlying theory and its implementation
From MaRDI portal
Publication:5015602
DOI10.3233/SAT190115zbMATH Open1484.68225OpenAlexW2995789353MaRDI QIDQ5015602FDOQ5015602
Authors: Ralf Wimmer, Christoph Scholl, Bernd Becker 
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
Recommendations
Cites Work
- bv2epr: a tool for polynomially translating quantifier-free bit-vector formulas into EPR
- sQueezeBF: an effective preprocessor for QBFs based on equivalence reasoning
- Blocked clause elimination for QBF
- Theory and Applications of Satisfiability Testing
- A structure-preserving clause form translation
- Resolution for quantified Boolean formulas
- Solving QBF with counterexample guided refinement
- Title not available (Why is that?)
- Bounded Universal Expansion for Preprocessing QBF
- Algorithms for computing backbones of propositional formulae
- Title not available (Why is that?)
- Depth-First Search and Linear Graph Algorithms
- Theory and Applications of Satisfiability Testing
- Dependency learning for QBF
- The complexity of theorem-proving procedures
- SAT-Based Synthesis Methods for Safety Specs
- Title not available (Why is that?)
- GRASP: a search algorithm for propositional satisfiability
- Lower bounds for multiplayer noncooperative games of incomplete information
- Backdoor sets of quantified Boolean formulas
- Computing Resolution-Path Dependencies in Linear Time ,
- Quantifier reordering for QBF
- Variable independence and resolution paths for quantified Boolean formulas
- iProver – An Instantiation-Based Theorem Prover for First-Order Logic (System Description)
- Theory and Applications of Satisfiability Testing
- Bounded model checking using satisfiability solving
- Blocked clause elimination
- Title not available (Why is that?)
- Toward leaner binary-clause reasoning in a satisfiability solver
- On a generalization of extended resolution
- Title not available (Why is that?)
- Applications of SAT Solvers to Cryptanalysis of Hash Functions
- Efficient CNF simplification based on binary implication graphs
- Clause elimination procedures for CNF formulas
- Complexity results for classes of quantificational formulas
- Incremental preprocessing methods for use in BMC
- Theory and Applications of Satisfiability Testing
- Henkin quantifiers and Boolean formulae: a certification perspective of DQBF
- Dependency Quantified Horn Formulas: Models and Complexity
- An algorithm to evaluate quantified Boolean formulae and its experimental evaluation
- Efficient SAT-based bounded model checking for software verification
- DepQBF 6.0: a search-based QBF solver beyond traditional QCDCL
- Variable Dependencies of Quantified CSPs
- Soundness of \(\mathcal{Q}\)-resolution with dependency schemes
- Thread-parallel integrated test pattern generator utilizing satisfiability analysis
- A resolution-style proof system for DQBF
- From DQBF to QBF by dependency elimination
- Skolem functions for DQBF
- Clausal abstraction for DQBF
- Fast DQBF Refutation
- Preprocessing for DQBF
- Clause elimination for SAT and QSAT
- Dependency schemes for DQBF
- Efficiently representing existential dependency sets for expansion-based QBF solvers
Cited In (8)
- Certified DQBF solving by definition extraction
- DQBDD: an efficient BDD-based DQBF solver
- Dependency schemes in CDCL-based QBF solving: a proof-theoretic study
- Solving dependency quantified Boolean formulas using quantifier localization
- On preprocessing for weighted MaxSAT
- QRATPre+: effective QBF preprocessing via strong redundancy properties
- Using decomposition-parameters for QBF: mind the prefix!
- sQueezeBF: an effective preprocessor for QBFs based on equivalence reasoning
Uses Software
This page was built for publication: The (D)QBF preprocessor HQSpre -- underlying theory and its implementation
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5015602)
