Variants of Tagged Sentential Decision Diagrams

--A recently proposed canonical form of Boolean functions, namely tagged sentential decision diagrams (TSDDs), exploits both the standard and zero-suppressed trimming rules. The standard ones minimize the size of sentential decision diagrams (SDDs) while the zero-suppressed trimming rules have the same objective as the standard ones but for zero-suppressed sentential decision diagrams (ZSDDs). The original TSDDs, which we call zero-suppressed TSDDs (ZTSDDs), firstly fully utilize the zero-suppressed trimming rules, and then the standard ones. In this paper, we present a variant of TSDDs which we call standard TSDDs (STSDDs) by reversing the order of trimming rules. We then prove the canonicity of STSDDs and present the algorithms for binary operations on TSDDs. In addition, we offer two kinds of implementations of STSDDs and ZTSDDs and acquire three variations of the original TSDDs. Experimental evaluations demonstrate that the four versions of TSDDs have the size advantage over SDDs and ZSDDs. Knowledge compilation aims to transform a Boolean function into a tractable representation. Binary decision diagrams (BDDs) [1] is one of the most notable representations that is widely employed for numerous fields of computer science including computer-aided design [2], [3], cryptography [4], [5], formal method [6], [7]. Interestingly, BDDs are a canonical form under the two restrictions: ordering and reduction, that means, any Boolean function has a unique BDD representation. This property reduces the storage space of BDDs and enables an O (1) time equality-test on BDDs. Following the success of BDDs, a variant zero-suppressed BDDs (ZDDs) was proposed in [8]. ZDDs enjoy the same properties: canonicity and supporting polytime Boolean operations as BDDs.