Ordered Binary Decision Diagrams and the Davis-Putnam procedure

DOI10.1007/BFb0016843zbMath1495.68202MaRDI QIDQ5096299

T. E. Uribe, Mark E. Stickel

Publication date: 16 August 2022

Published in: Constraints in Computational Logics (Search for Journal in Brave)

Mathematics Subject Classification ID

03B35: Mechanization of proofs and logical operations

68T20: Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)

03B05: Classical propositional logic

68V15: Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)

Related Items

On sets, types, fixed points, and checkerboards, Building decision procedures for modal logics from propositional decision procedures — The case study of modal K, Unnamed Item, Generating Extended Resolution Proofs with a BDD-Based SAT Solver, Resolution and binary decision diagrams cannot simulate each other polynomially, A satisfiability procedure for quantified Boolean formulae, Building decision procedures for modal logics from propositional decision procedures: The case study of modal \(K(m)\)., Formal verification based on Boolean expression diagrams, Generating extended resolution proofs with a BDD-based SAT solver, ProCount: weighted projected model counting with graded project-join trees

Cites Work

• Unnamed Item
• Unnamed Item
• Refutational theorem proving using term-rewriting systems
• Embedding Boolean expressions into logic programming
• Symbolic model checking: \(10^{20}\) states and beyond
• Introduction to the OBDD algorithm for the ATP community
• Automated reasoning and exhaustive search: Quasigroup existence problems
• On the complexity of VLSI implementations and graph representations of Boolean functions with application to integer multiplication
• Graph-Based Algorithms for Boolean Function Manipulation
• Finding the optimal variable ordering for binary decision diagrams
• A Computing Procedure for Quantification Theory
• A machine program for theorem-proving