Two solutions to incorporate zero, successor and equality in binary decision diagrams

In this article we extend BDDs (binary decision diagrams) for plain propositional logic to the fragment of first order logic, consisting of quantifier free logic with equality, zero and successor. We insert equations with zero and successor in BDDs, and call these objects (0,S,=)-BDDs. We extend the notion of {em Ordered} BDDs in the presence of equality, zero and successor. (0,S,=)-BDDs can be transformed to equivalent Ordered (0,S,=)-BDD s by applying a number of rewrite rules. All paths in these extended OBDDs are satisfiable. The major advantage of transforming a formula to an equivalent Ordered (0,S,=)-BDD is that on the latter it can be observed in constant time whether the formula is a tautology, a contradiction, or just satisfiable.