Preprocessing for DQBF

DOI10.1007/978-3-319-24318-4_13MaRDI QIDQ3453223zbMATH OpenOpenAlexFDO

Authors Ralf Wimmer, Karina Gitina, Jennifer Nist, Christoph Scholl, Bernd Becker

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

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)

Recommendations

• Preprocessing DEA
• Preprocessing for quadratic programming
• Preprocessing of intractable problems
• Dependency schemes for DQBF
• Preprocessing predicates and queries
• Prefolding in FHT algorithms
• Preprocessing under uncertainty
• Demand Queries with Preprocessing
• Preconditioning

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 5493266 (Why is no real title available?)
• Algorithms for computing backbones of propositional formulae
• Applications of SAT Solvers to Cryptanalysis of Hash Functions
• Backdoor sets of quantified Boolean formulas
• Blocked clause elimination
• Blocked clause elimination for QBF
• Clause elimination procedures for CNF formulas
• Computing Resolution-Path Dependencies in Linear Time ,
• Dependency Quantified Horn Formulas: Models and Complexity
• Depth-First Search and Linear Graph Algorithms
• Efficient CNF simplification based on binary implication graphs
• Efficiently representing existential dependency sets for expansion-based QBF solvers
• Fast DQBF Refutation
• Henkin quantifiers and Boolean formulae: a certification perspective of DQBF
• Incremental QBF solving by DepQBF
• Lower bounds for multiplayer noncooperative games of incomplete information
• Preprocessing for DQBF
• 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
• sQueezeBF: an effective preprocessor for QBFs based on equivalence reasoning

Cited in

(12)

• Dependency schemes for DQBF
• The (D)QBF preprocessor HQSpre -- underlying theory and its implementation
• Interpolation-based semantic gate extraction and its applications to QBF preprocessing
• Preprocessing Boolean formulae for BDDs in a probabilistic context
• Lifting QBF resolution calculi to DQBF
• Building strategies into QBF proofs
• Solving dependency quantified Boolean formulas using quantifier localization
• Dynamic blocked clause elimination for projected model counting
• Preprocessing for DQBF
• QRATPre+: effective QBF preprocessing via strong redundancy properties
• sQueezeBF: an effective preprocessor for QBFs based on equivalence reasoning
• Blocked clause elimination for QBF

Describes a project that uses

Uses Software

• Quantor
• Coprocessor
• Easychair
• DepQBF
• Bloqqer
• sQueezeBF
• MiniSat

This page was built for publication: Preprocessing for DQBF

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3453223)