Compiling graph substructures into sentential decision diagrams

Abstract

The Zero-suppressed Sentential Decision Diagram (ZSDD) is a recently discovered tractable representation of Boolean functions. ZSDD subsumes the Zero-suppressed Binary Decision Diagram (ZDD) as a strict subset, and similar to ZDD, it can perform several useful operations like model counting and Apply operations. We propose a top-down compilation algorithm for ZSDD that represents sets of specific graph substructures, e.g., matchings and simple paths of a graph. We experimentally confirm that the proposed algorithm is faster than other construction methods including bottom-up methods and top-down methods for ZDDs, and the resulting ZSDDs are smaller than ZDDs representing the same graph substructures. We also show that the size constructed ZSDDs can be bounded by the branch-width of the graph. This bound is tighter than that of ZDDs.