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

Mechanization of proofs and logical operations (03B35) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Classical propositional logic (03B05) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items

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, Formal verification based on Boolean expression diagrams, On sets, types, fixed points, and checkerboards, Building decision procedures for modal logics from propositional decision procedures — The case study of modal K, Generating extended resolution proofs with a BDD-based SAT solver, Unnamed Item, Building decision procedures for modal logics from propositional decision procedures: The case study of modal \(K(m)\)., 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