A satisfiability procedure for quantified Boolean formulae

DOI10.1016/S0166-218X(02)00409-2zbMath1029.68082MaRDI QIDQ1408385

Yunshan Zhu, Armin Biere, David Alan Plaisted

Publication date: 15 September 2003

Published in: Discrete Applied Mathematics (Search for Journal in Brave)

zbMATH Keywords

SatisfiabilityQBFModel checkingBDDsCircuit verificationCut widthDavis and Putnam procedure

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25)

Related Items

Effective use of Boolean satisfiability procedures in the formal verification of superscalar and VLIW microprocessors., Quantifier elimination by dependency sequents, Abstraction-Based Algorithm for 2QBF, A Unified Framework for Certificate and Compilation for QBF

Uses Software

• SATO
• Leibniz
• ZRes

Cites Work

• A structure-preserving clause form translation
• Symbolic model checking: \(10^{20}\) states and beyond
• Resolution for quantified Boolean formulas
• The propositional formula checker HeerHugo
• Resolution versus search: Two strategies for SAT
• Graph-Based Algorithms for Boolean Function Manipulation
• Ordered Binary Decision Diagrams and the Davis-Putnam procedure
• SATO: An efficient propositional prover
• A Computing Procedure for Quantification Theory
• A machine program for theorem-proving
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item