Tagged Sentential Decision Diagrams: Combining Standard and Zero-suppressed Compression and Trimming Rules

The Sentential Decision Diagram (SDD) is a compact and canonical representation of Boolean functions that generalizes the Ordered Binary Decision Diagrams (OBDDs). A variant of SDDs, namely Zero-suppressed Sentential Decision Diagrams (ZSDDs), was proposed recently by using different trimming rules. SDDs are suitable for functions where adjacent input assignments have the same outcome, while ZSDDs are more compact for spare functions. In this paper, we introduce a novel canonical SDD variant, called the Tagged Sentential Decision Diagrams (TSDDs). The key insight of TSDDs is to combine both trimming rules of SDDs and ZSDDs. With both characteristics of SDDs and ZSDDs, the TSDD representation is at least as small as the SDD or ZSDD representation for any Boolean functions. This is also shown in our experimental evaluation.