Davis and Putnam meet Henkin: solving DQBF with resolution

DOI10.1007/978-3-030-80223-3_4MaRDI QIDQ2118283zbMATH OpenOpenAlexFDO

Authors Joshua Blinkhorn, Tomáš Peitl, Friedrich Slivovsky

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

Analysis of algorithms and problem complexity (68Q25) Computational aspects of satisfiability (68R07) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)

Cites work

• A Computing Procedure for Quantification Theory
• A structure-preserving clause form translation
• Building strategies into QBF proofs
• Clausal abstraction for DQBF
• Dependency Quantified Horn Formulas: Models and Complexity
• Encodings of bounded synthesis
• Graph-Based Algorithms for Boolean Function Manipulation
• Henkin quantifiers and Boolean formulae: a certification perspective of DQBF
• scientific article; zbMATH DE number 3560737 (Why is no real title available?)
• scientific article; zbMATH DE number 1946853 (Why is no real title available?)
• scientific article; zbMATH DE number 3313427 (Why is no real title available?)
• Incremental determinization
• Lower bounds for multiplayer noncooperative games of incomplete information
• Resolution for quantified Boolean formulas
• Resolution Trees with Lemmas: Resolution Refinements that Characterize DLL Algorithms with Clause Learning
• Small Stone in pool
• Theory and Applications of Satisfiability Testing

Cited in

(5)

• A resolution proof system for dependency stochastic Boolean satisfiability
• Transforming quantified Boolean formulas using biclique covers
• QBF merge resolution is powerful but unnatural
• Hard QBFs for merge resolution
• Extending merge resolution to a family of QBF-proof systems

Describes a project that uses

Uses Software

• dCAQE

This page was built for publication: Davis and Putnam meet Henkin: solving DQBF with resolution

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