Davis and Putnam meet Henkin: solving DQBF with resolution
From MaRDI portal
Publication:2118283
DOI10.1007/978-3-030-80223-3_4OpenAlexW3185782780MaRDI QIDQ2118283
Friedrich Slivovsky, Tomáš Peitl, Joshua Blinkhorn
Publication date: 22 March 2022
Full work available at URL: https://doi.org/10.1007/978-3-030-80223-3_4
Analysis of algorithms and problem complexity (68Q25) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Computational aspects of satisfiability (68R07)
Related Items
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- A structure-preserving clause form translation
- Resolution for quantified Boolean formulas
- Building strategies into QBF proofs
- Clausal abstraction for DQBF
- Henkin quantifiers and Boolean formulae: a certification perspective of DQBF
- Incremental Determinization
- Encodings of Bounded Synthesis
- Resolution Trees with Lemmas: Resolution Refinements that Characterize DLL Algorithms with Clause Learning
- Graph-Based Algorithms for Boolean Function Manipulation
- Theory and Applications of Satisfiability Testing
- Small Stone in Pool
- A Computing Procedure for Quantification Theory
- Dependency Quantified Horn Formulas: Models and Complexity
- Lower bounds for multiplayer noncooperative games of incomplete information