Dependency Schemes for DQBF

DOI10.1007/978-3-319-40970-2_29zbMath1475.68225OpenAlexW2482896395MaRDI QIDQ2818034

Ralf Wimmer, Christoph Scholl, Karina Wimmer, Bernd Becker

Publication date: 5 September 2016

Published in: Theory and Applications of Satisfiability Testing – SAT 2016 (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-319-40970-2_29

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15) Computational aspects of satisfiability (68R07)

Related Items

Reinterpreting dependency schemes: soundness meets incompleteness in DQBF, The (D)QBF Preprocessor HQSpre – Underlying Theory and Its Implementation1, Certified DQBF solving by definition extraction

Uses Software

• Quantor

Cites Work

• Unnamed Item
• Quantifier reordering for QBF
• Soundness of \(\mathcal{Q}\)-resolution with dependency schemes
• Thread-parallel integrated test pattern generator utilizing satisfiability analysis
• Backdoor sets of quantified Boolean formulas
• Henkin quantifiers and Boolean formulae: a certification perspective of DQBF
• Planning as satisfiability: parallel plans and algorithms for plan search
• Computing Resolution-Path Dependencies in Linear Time ,
• SAT-Based Synthesis Methods for Safety Specs
• Variable Independence and Resolution Paths for Quantified Boolean Formulas
• Fast DQBF Refutation
• Preprocessing for DQBF
• Bounded Universal Expansion for Preprocessing QBF
• Integrating Dependency Schemes in Search-Based QBF Solvers
• Efficiently Representing Existential Dependency Sets for Expansion-based QBF Solvers
• Theory and Applications of Satisfiability Testing
• Dependency Quantified Horn Formulas: Models and Complexity
• Bounded model checking using satisfiability solving
• Lower bounds for multiplayer noncooperative games of incomplete information