Davis and Putnam meet Henkin: solving DQBF with resolution
From MaRDI portal
Publication:2118283
DOI10.1007/978-3-030-80223-3_4MaRDI 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
68Q25: Analysis of algorithms and problem complexity
68T20: Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)
68R07: Computational aspects of satisfiability
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