From DQBF to QBF by dependency elimination

DOI10.1007/978-3-319-66263-3_21zbMATH Open1496.68372OpenAlexW2744754855MaRDI QIDQ1680263FDOQ1680263

Authors: Ralf Wimmer, Andreas Karrenbauer, Ruben Becker, Christoph Scholl, Bernd Becker 

Publication date: 15 November 2017

Full work available at URL: https://doi.org/10.1007/978-3-319-66263-3_21

Recommendations

• Dependency schemes for DQBF
• Dependency Quantified Boolean Formulas: An Overview of Solution Methods and Applications
• Dependency learning for QBF
• Integrating dependency schemes in search-based QBF solvers
• Dependency Learning for QBF

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cited In (11)

• Dependency Learning for QBF
• Certified DQBF solving by definition extraction
• DQBDD: an efficient BDD-based DQBF solver
• DepQBF 6.0: a search-based QBF solver beyond traditional QCDCL
• Solving dependency quantified Boolean formulas using quantifier localization
• Shortening QBF proofs with dependency schemes
• Rewriting (dependency-)quantified 2-CNF with arbitrary free literals into existential 2-HORN
• Quantifier elimination by dependency sequents
• The (D)QBF Preprocessor HQSpre – Underlying Theory and Its Implementation1
• Dependency Quantified Boolean Formulas: An Overview of Solution Methods and Applications
• Strong (D)QBF dependency schemes via tautology-free resolution paths

This page was built for publication: From DQBF to QBF by dependency elimination

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