Partial implicit unfolding in the Davis-Putnam procedure for quantified Boolean formulae

DOI10.1007/3-540-45653-8_25MaRDI QIDQ2996176zbMATH OpenOpenAlexFDO

Authors Jussi Rintanen

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

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Analysis of algorithms and problem complexity (68Q25)

Recommendations

• A satisfiability procedure for quantified Boolean formulae
• An algorithm to evaluate quantified Boolean formulae and its experimental evaluation
• An algorithm to evaluate quantified Boolean formulae and its experimental evaluation
• Contributions to the theory of practical quantified Boolean formula solving
• Theory and Applications of Satisfiability Testing

Cited in

(11)

• A self-adaptive multi-engine solver for quantified Boolean formulas
• A satisfiability procedure for quantified Boolean formulae
• An algorithm to evaluate quantified Boolean formulae and its experimental evaluation
• Programming for modular reconfigurable robots
• An algorithm to evaluate quantified Boolean formulae and its experimental evaluation
• Compressing BMC encodings with QBF
• Resolution and Expressiveness of Subclasses of Quantified Boolean Formulas and Circuits
• Message passing algorithm for solving QBF using more reasoning
• Formal methods for NFA equivalence: QBFs, witness extraction, and encoding verification
• SAT-based planning in complex domains: Concurrency, constraints and nondeterminism
• Models and quantifier elimination for quantified Horn formulas

This page was built for publication: Partial implicit unfolding in the Davis-Putnam procedure for quantified Boolean formulae

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