Davis and Putnam meet Henkin: solving DQBF with resolution

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

Mathematics Subject Classification ID

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

A resolution proof system for dependency stochastic Boolean satisfiability

Uses Software

• dCAQE

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