Ordered Binary Decision Diagrams and the Davis-Putnam procedure
From MaRDI portal
Publication:5096299
DOI10.1007/BFb0016843zbMath1495.68202MaRDI QIDQ5096299
Publication date: 16 August 2022
Published in: Constraints in Computational Logics (Search for Journal in Brave)
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