Partial Implicit Unfolding in the Davis-Putnam Procedure for Quantified Boolean Formulae
From MaRDI portal
Publication:2996176
DOI10.1007/3-540-45653-8_25zbMath1275.03082OpenAlexW1597057550MaRDI QIDQ2996176
Publication date: 6 May 2011
Published in: Logic for Programming, Artificial Intelligence, and Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/3-540-45653-8_25
Analysis of algorithms and problem complexity (68Q25) Mechanization of proofs and logical operations (03B35)
Related Items
Formal methods for NFA equivalence: QBFs, witness extraction, and encoding verification, Message passing algorithm for solving QBF using more reasoning, Models and quantifier elimination for quantified Horn formulas, Programming for modular reconfigurable robots, A self-adaptive multi-engine solver for quantified Boolean formulas, Compressing BMC Encodings with QBF, SAT-based planning in complex domains: Concurrency, constraints and nondeterminism