Introduction to the OBDD algorithm for the ATP community

DOI10.1007/BF00881842zbMath0804.68136OpenAlexW2158114636MaRDI QIDQ1332638

J. Strother Moore

Publication date: 12 January 1995

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/bf00881842

zbMATH Keywords

ordered binary decision diagramsnormalized IF expressionspropositional equivalence

Mathematics Subject Classification ID

Related Items

Ordered Binary Decision Diagrams and the Davis-Putnam procedure, Automatic verification of reduction techniques in higher order logic, Applying Light-Weight Theorem Proving to Debugging and Verifying Pointer Programs, Simplification of boolean verification conditions

Uses Software

• NQTHM
• ROBDD

Cites Work

• Unnamed Item
• Automated reasoning and exhaustive search: Quasigroup existence problems
• Graph-Based Algorithms for Boolean Function Manipulation