Basing Decisions on Sentences in Decision Diagrams

Abstract

The Sentential Decision Diagram (SDD) is a recently proposed representation of Boolean functions, containing Ordered Binary Decision Diagrams (OBDDs) as a distinguished subclass. While OBDDs are characterized by total variable orders, SDDs are characterized by dissections of variable orders, known as vtrees. Despite this generality, SDDs retain a number of properties, such as canonicity and a polytime Apply operator, that have been critical to the practical success of OBDDs. Moreover, upper bounds on the size of SDDs were also given, which are tighter than comparable upper bounds on the size of OBDDs. In this paper, we analyze more closely some of the theoretical properties of SDDs and their size. In particular, we consider the impact of basing decisions on sentences (using dissections as in SDDs), in comparison to basing decisions on variables (using total variable orders as in OBDDs). Here, we identify a class of Boolean functions where basing decisions on sentences using dissections of a variable order can lead to exponentially more compact SDDs, compared to OBDDs based on the same variable order. Moreover, we identify a fundamental property of the decompositions that underlie SDDs and use it to show how certain changes to a vtree can also lead to exponential differences in the size of an SDD.