Zero, successor and equality in BDDs

We extend BDDs (binary decision diagrams) for plain propositional logic to the fragment of first order logic, consisting of quantifier free logic with zero, successor and equality. We allow equations with zero and successor in the nodes of a BDD, and call such objects ( 0 , S , = ) -BDDs. We extend the notion of Ordered BDDs in the presence of zero, successor and equality. ( 0 , S , = ) -BDDs can be transformed to equivalent Ordered ( 0 , S , = ) -BDDs by applying a number of rewrite rules until a normal form is reached. All paths in these ordered ( 0 , S , = ) -BDDs represent satisfiable conjunctions. 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.