SI2 - SSE: A Next-Generation Decision Diagram Library

有各种各样的科学问题，由于必须考虑和评估极其大量的可能性，因此很难解决。通常，困难是由大量相互作用的组件的组合引起的，即使单个组件相对简单。相关的实际问题是测量链路可能失效的通信网络的可靠性（由于网络中不同通信路径的数量而变得困难），或者确定汽车的制动器将始终工作（由于汽车中相互作用的软件和硬件组件的组合的数量而变得困难），或者确定一个发电机的故障不会导致影响国家电网大部分的级联故障。这类问题在概念上类似于寻找魔方的最优解（由于大量不同的可能配置而变得困难），或者在国际象棋中，确定国际象棋中是否存在一系列移动，使得白色总是可以获胜（由于大量不同的可能国际象棋游戏而变得困难）。这个项目的目标是开发一个名为Meddly的软件库，各种应用程序可以使用它来构建和表示这些类型的组合问题的解决方案。Meddly的底层技术是决策图，这是一种组织数据的机制，可以在计算过程中自动发现和利用重复的模式或子模式。该项目将增加决策图技术的功能，有助于促进对这项技术的理解，并将其应用于更多类型的问题。来自世界各地的几位研究人员对Meddly表示了兴趣，作为该项目的一部分，开发人员将协助这些研究人员将Meddly集成到现有的工具中，然后将其应用于真实的问题。该项目还具有教育目标，通过学生参与项目，并将这项工作纳入现有课程。许多基于计算机的科学或工程应用程序需要存储，分析和操作大量数据。通常，这种数据具有足够的结构，专用数据结构和算法可以比显式方法具有更小的内存和时间需求。一个重要的例子是硬件和软件的符号验证，传统上，二元决策图（BDD）已成功地用于研究具有巨大状态空间的系统。已经出现了一些用于BDD的软件库来支持这些操作，并且BDD已经被应用于各种应用程序，作为利用通常隐藏的结构的手段。然而，在过去的十年中，决策图理论继续发展，通过将BDD推广到具有多路决策（MDD），多路或数值结果或边值的变体来编码实值数据，并通过提出各种简化规则来改变（通常缩小）决策图形状，以及许多重要的算法改进。不幸的是，决策图库并没有跟上这些理论的发展。拟议的工作旨在填补这一空白，通过合并和扩展两个现有的原型库开发的两个invesigators，Meddly和TEDDY，成为一个强大的，下一代决策图库，支持更一般的决策图理论。新的库将包括（1）非二进制变量，包括先验无界离散域，甚至在某些限制下的无限域，（2）非布尔函数值，附加到终端节点或决策图的边缘，以及（3）更一般的规范性定义，包括广泛的约简规则。一些建议的活动将有助于平滑用户采用此库的学习曲线，从用户手册，教程，示例，wiki和用户组等已被证明的方法到新颖的方法，如开发可视化技术以帮助调试和理解决策图。拟议的软件将推动决策图库支持远远超出今天的典型BDD库的能力，允许令人兴奋的新应用程序出现在不同的领域远远超出经典的，如符号模型检查。此外，拟议的研究活动将提高我们对决策图技术的理解，为结构化函数及其表示的性质提供深入的新见解。 这有可能在目前利用决策图的领域中推进最先进的技术，因为改进的库支持可以导致解决前所未有大小的问题实例的能力，并且在实现所提出的决策图变体的库的可用性将允许研究人员使用基于决策图的新方法来解决经典问题的领域中。下一代决策图库将通过改进管理大型结构化数据的软件应用程序，对从工程到计算机科学理论再到生物学的学科产生积极影响。支持信证明，全球许多研究小组都渴望在其工具中包含更通用、更强大的决策图功能。预期的教育影响包括开发公开的在线教程;为本科生和研究生提供研究、实施和实验机会;以及通过讲座、作业和项目将开发的技术和软件整合到现有课程中。从拟议的活动产生的基本理论和开发的软件将加强概念，学生将保留和应用在他们的职业生涯。

There are a variety of scientific problems whose solution is made difficult because of the extremely large number of possibilities that must be considered and evaluated. Often, the difficulty is caused by a large number of combinations of interacting components, even though the individual components are relatively simple. Relevant practical problems are measuring the reliability of a communication network where links may fail (made difficult by the number of different communication paths in the network), or determining that an automobile's brakes will always work (made difficult by the number of combinations of the interacting software and hardware components in an automobile), or determining that the failure of one power generator will not cause a cascading failure that affects a large portion of the nation's power grid. This class of problem is conceptually similar to finding an optimal solution for Rubik's cube (which is made difficult by the large number of different possible configurations) or, in chess, determining if there is a sequence of moves in chess such that white can always force a win (made difficult by the huge number of different possible chess games). The goal of this project is to develop a software library called Meddly that various applications can use to build and represent solutions to these types of combinatoric problems. The underlying technology of Meddly is decision diagrams, a mechanism for organizing data in such a way that repeated patterns or subpatterns are automatically discovered and exploited during computation. The project will add to the capabilities of decision diagram technology, help to advance the understanding of this technology as well as apply it to more types of problems. Several researchers from around the world have expressed interest in Meddly, and as part of this project, developers will assist those researchers to integrate Meddly into existing tools, which will then be applied to real problems. The project also has educational goals, through the engagement of students in the project, and the incorporation of this work in existing courses.Many computer-based scientific or engineering applications need to store, analyze, and manipulate large data. Often, this data has enough structure that specialized data structures and algorithms can have dramatically smaller memory and time requirements than explicit approaches. An important such case is symbolic verification of hardware and software, where, traditionally, binary decision diagrams (BDDs) have been successfully employed to study systems with enormous state spaces. Several software libraries for BDDs have arisen to support these operations, and BDDs have been applied to diverse applications as a means to exploit structure that is often hidden. However, in the past decade, decision diagram theory has continued to advance, by generalizing BDDs to variants with multi-way decisions (MDDs), multi-way or numerical outcomes, or edge values to encode real-valued data, and by proposing a variety of reduction rules to change (and often shrink) the decision diagram shape, as well as many important algorithmic improvements. Unfortunately, decision diagram libraries have not kept up with these theoretical advances. The proposed work seeks to fill this gap, by merging and expanding two existing prototype libraries developed by the two invesigators, Meddly and TEDDY, into a powerful, next-generation decision diagram library that supports a more general theory of decision diagrams. The new library will encompass (1) non-binary variables, including a-priori unbounded discrete domains and even infinite domains under certain restrictions, (2) non-boolean function values, attached either to terminal nodes or to the edges of the decision diagram, and (3) a more general definition of canonicitythat includes a wide spectrum of reduction rules. Several proposed activities will help smooth the learning curve for users adopting this library, from proven methods such as user manuals, tutorials, examples, wikis, and user groups, to novel ones such as the development of visualization techniques to aid the debugging and understanding of decision diagrams. The proposed software will push decision diagram library support far beyond the capabilities of today's typical BDD libraries, allowing exciting new applications to emerge in diverse fields well beyond classic ones such as symbolic model checking. Additionally, the proposed research activities will improve our understanding of decision diagram technology, providing deep new insights into the nature of structured functions and their representations. This has the potential to advance the state of the art both in fields that currently utilize decision diagrams, as improved library support can lead to the ability to tackle problem instances of unprecedented size, and in fields where the availability of a library implementing the proposed decision diagram variants will allow researchers to tackle classic problems with novel approaches based on decision diagrams. A next-generation decision diagram library will positively impact disciplines ranging from engineering to computer science theory to biology, via improved software applications that manage large and structured data. Letters of support attest to the many research groups worldwide eager to include more general and powerful decision diagram capabilities in their tools. The anticipated educational impact includes development of publicly available online tutorials; research, implementation, and experimentation opportunities for both undergraduate and graduate students; and integration of the developed techniques and software into existing courses via lectures, assignments, and projects. The underlying theory and developed software resulting from the proposed activities will reinforce concepts that students will retain and apply during their careers.