The (D)QBF preprocessor HQSpre -- underlying theory and its implementation
From MaRDI portal
Publication:5015602
Recommendations
Cites work
- scientific article; zbMATH DE number 5719280 (Why is no real title available?)
- scientific article; zbMATH DE number 3560737 (Why is no real title available?)
- scientific article; zbMATH DE number 1305704 (Why is no real title available?)
- scientific article; zbMATH DE number 3325539 (Why is no real title available?)
- scientific article; zbMATH DE number 3196255 (Why is no real title available?)
- A resolution-style proof system for DQBF
- A structure-preserving clause form translation
- Algorithms for computing backbones of propositional formulae
- An algorithm to evaluate quantified Boolean formulae and its experimental evaluation
- Applications of SAT Solvers to Cryptanalysis of Hash Functions
- Backdoor sets of quantified Boolean formulas
- Blocked clause elimination
- Blocked clause elimination for QBF
- Bounded Universal Expansion for Preprocessing QBF
- Bounded model checking using satisfiability solving
- Clausal abstraction for DQBF
- Clause elimination for SAT and QSAT
- Clause elimination procedures for CNF formulas
- Complexity results for classes of quantificational formulas
- Computing Resolution-Path Dependencies in Linear Time ,
- DepQBF 6.0: a search-based QBF solver beyond traditional QCDCL
- Dependency Quantified Horn Formulas: Models and Complexity
- Dependency learning for QBF
- Dependency schemes for DQBF
- Depth-First Search and Linear Graph Algorithms
- Efficient CNF simplification based on binary implication graphs
- Efficient SAT-based bounded model checking for software verification
- Efficiently representing existential dependency sets for expansion-based QBF solvers
- Fast DQBF Refutation
- From DQBF to QBF by dependency elimination
- GRASP: a search algorithm for propositional satisfiability
- Henkin quantifiers and Boolean formulae: a certification perspective of DQBF
- Incremental preprocessing methods for use in BMC
- Lower bounds for multiplayer noncooperative games of incomplete information
- On a generalization of extended resolution
- Preprocessing for DQBF
- Quantifier reordering for QBF
- Resolution for quantified Boolean formulas
- SAT-Based Synthesis Methods for Safety Specs
- Skolem functions for DQBF
- Solving QBF with counterexample guided refinement
- Soundness of \(\mathcal{Q}\)-resolution with dependency schemes
- The complexity of theorem-proving procedures
- Theory and Applications of Satisfiability Testing
- Theory and Applications of Satisfiability Testing
- Theory and Applications of Satisfiability Testing
- Theory and Applications of Satisfiability Testing
- Thread-parallel integrated test pattern generator utilizing satisfiability analysis
- Toward leaner binary-clause reasoning in a satisfiability solver
- Variable Dependencies of Quantified CSPs
- Variable independence and resolution paths for quantified Boolean formulas
- bv2epr: a tool for polynomially translating quantifier-free bit-vector formulas into EPR
- iProver – An Instantiation-Based Theorem Prover for First-Order Logic (System Description)
- sQueezeBF: an effective preprocessor for QBFs based on equivalence reasoning
Cited in
(8)- Certified DQBF solving by definition extraction
- DQBDD: an efficient BDD-based DQBF solver
- Solving dependency quantified Boolean formulas using quantifier localization
- Dependency schemes in CDCL-based QBF solving: a proof-theoretic study
- 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
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)
