BIB-VERSION:: CS-TR-v2.0
          ID:: SBCS//stark/peq-bdd.pdf
       ENTRY:: July 2, 2008
ORGANIZATION:: State University of New York at Stony Brook, Computer Science
       TITLE:: Linear Decision Diagrams
        TYPE:: Technical Report
      AUTHOR:: Song, Wenxin and Stark, Eugene W.
     CONTACT:: Eugene W. Stark, Department of Computer Science,
                   SUNY at Stony Brook, Stony Brook, NY 11794-4400
                   Tel: 631-632-8444 <stark@cs.sunysb.edu>
        DATE:: July 2, 2008
   RETRIEVAL:: HTTP from BSD7.CS.SUNYSB.EDU with the URL
		   http://bsd7.cs.sunysb.edu/~stark/REPORTS/peq-bdd.abstract

ABSTRACT::

A positive equational formula (PEF) is a negation-free open
formula in the language of pure equality. In this paper, we present a normal
form for positive equational formulas that lends itself readily to the
representation of such formulas using ordered binary decision diagrams
(BDDs) whose nodes are labeled by equations. In contrast to previous
work of Groote and van de Pol that treated the larger class of equational
formulas with negation, we show that our normal forms for PEFs
are unique in the sense that two normal forms are logically equivalent
if and only if they are identical. This result means that a BDD-based
representation of our normal forms can implement equivalence checking
for PEFs in constant time, as well as avoid space inefficiency that could
otherwise result from storing multiple syntactically distinct variants of
a formula. We present a recursive algorithm that traverses an arbitrary
PEF given as input and builds an equivalent normal form in a bottomup
fashion. In addition, we apply ideas from the reduction algorithm to
obtain bottom-up, normal-form-preserving algorithms for various logical
operations on PEFs.