Clausal abstraction for DQBF

DOI10.1007/978-3-030-24258-9_27zbMath1441.68241arXiv1808.08759OpenAlexW2947743331MaRDI QIDQ2181947

Leander Tentrup, Markus N. Rabe

Publication date: 20 May 2020

Full work available at URL: https://arxiv.org/abs/1808.08759

Mathematics Subject Classification ID

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

Related Items (8)

Solving dependency quantified Boolean formulas using quantifier localization ⋮ Building strategies into QBF proofs ⋮ dCAQE ⋮ The (D)QBF Preprocessor HQSpre – Underlying Theory and Its Implementation1 ⋮ CAQE and QuAbS: Abstraction Based QBF Solvers ⋮ Davis and Putnam meet Henkin: solving DQBF with resolution ⋮ Certified DQBF solving by definition extraction ⋮ DQBDD: an efficient BDD-based DQBF solver

Uses Software

• CAQE
• HQSpre
• BoSy

This page was built for publication: Clausal abstraction for DQBF