论文标题
可变偏移SDD：更简洁的句子决策图
Variable Shift SDD: A More Succinct Sentential Decision Diagram
论文作者
论文摘要
句子决策图（SDD）是布尔函数的可拖动表示，将著名有序的二进制决策图（OBDD）归为严格的子集。 SDD吸引了很多关注，因为它们比OBDD更简洁，并且具有规范形式并支持许多有用的查询和转换，例如模型计数和应用操作。在本文中，我们提出了一个更简洁的SDD变量，名为“变量Shift SDD”（VS-SDD）。关键思想是为在特定变量替换下等效的布尔函数创建独特的表示。我们表明，VS-SDD永远不会大于SDD，并且在某些情况下，VS-SDD的大小呈指数小于SDD的大小。此外，尽管如此简洁，我们表明，在Poly Time中支持的许多基本操作在Poly Time中也得到了VS-SDD的支持。实验证实，当应用于存在固有的对称性的经典计划实例时，VS-SDD比SDD更为简洁。
The Sentential Decision Diagram (SDD) is a tractable representation of Boolean functions that subsumes the famous Ordered Binary Decision Diagram (OBDD) as a strict subset. SDDs are attracting much attention because they are more succinct than OBDDs, as well as having canonical forms and supporting many useful queries and transformations such as model counting and Apply operation. In this paper, we propose a more succinct variant of SDD named Variable Shift SDD (VS-SDD). The key idea is to create a unique representation for Boolean functions that are equivalent under a specific variable substitution. We show that VS-SDDs are never larger than SDDs and there are cases in which the size of a VS-SDD is exponentially smaller than that of an SDD. Moreover, despite such succinctness, we show that numerous basic operations that are supported in polytime with SDD are also supported in polytime with VS-SDD. Experiments confirm that VS-SDDs are significantly more succinct than SDDs when applied to classical planning instances, where inherent symmetry exists.
