SHF: Medium: Improving the Efficiency and Applicability of Decision Diagrams

该项目扩展并改进了二进制决策图（bdd），二进制决策图是一种重要的技术，通过自动发现和利用模式，可以有效地解决各种应用领域中的组合问题。该项目的新颖之处在于增加了bdd可以利用的模式类型，并将几种不同的决策图统一到一个具有更广泛应用程序的一致框架中。该项目的影响是BDD技术的理论进步，对BDD解决方案技术的速度和内存效率的显著改进，使它们适合于过去不依赖于BDD的更广泛的应用领域，以及实现新BDD的开源软件库。该软件不仅便于对各种基准模型的工作进行评估，而且还降低了其他领域研究人员采用该软件的障碍。此外，该项目将研究成果纳入他们的研究生和本科课程。从历史上看，bdd存在两个主要但独立的版本：完全约简和零抑制，它们可以被视为利用不同类型模式的不同约简规则。这个项目包括将这两个简化规则以及新的规则整合到一个单一的结构中。这允许用户同时利用所有约简规则，而不必选择其中一个而不是另一个。同样，该项目整合了（历史上分离的）变量来表示非布尔函数，即多终端和边值bdd，并纳入了新的约简规则。框架设计（即约简规则和边缘值类型）由各种应用领域指导，包括bdd已经获得广泛成功的领域（模型检查、硬件验证和约束问题）和bdd在不久的将来有可能产生重大影响的领域（运动规划、物流和网络验证）。该项目的技术挑战包括开发规则，使特性的组合不会相互干扰（特别是，使每个函数在BDD中具有唯一的表示，即使应用了几个约简规则），改进BDD算法以利用新规则，并最终在软件库中有效地实现这些算法。该奖项反映了美国国家科学基金会的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

This project extends and improves binary decision diagrams (BDDs), an important technology that enables efficient solution for combinatorial problems in a variety of application domains, via automatic discovery and exploitation of patterns. The project's novelties are to increase the types of patterns that BDDs can utilize, and to unify several different varieties of decision diagrams into a single, consistent framework with broader applications. The project's impacts are theoretical advancements in BDD technology, significant improvements to the speed and memory efficiency of BDD solution techniques, making them suited to broader application areas that in the past have not relied on BDDs, and an open-source software library implementing the new BDDs. The software not only facilitates evaluation of the work on a variety of benchmark models, but also lowers the adoption barriers for researchers in other areas. In addition, the project incorporates research results in their graduate and undergraduate courses.Historically, BDDs exist in two main but separate versions: fully-reduced and zero-suppressed, which can be viewed as different reduction rules that exploit different types of patterns. This project involves integrating these two reduction rules, along with new ones, into a single structure. This allows users to exploit all the reduction rules simultaneously, without having to choose one over the other. Similarly, the project integrates (historically separated) variants to represent non-boolean functions, namely multi-terminal and edge-valued BDDs, and incorporates the new reduction rules. The framework design (i.e., reduction rules and edge value types) is guided by a variety of application domains, including both domains where BDDs have already enjoyed widespread success (model checking, hardware verification, and constraint problems) and domains where BDDs have potential to make substantial impact in the near future (motion planning, logistics, and network verification). The technical challenges of the project include developing rules so that the combination of features do not interfere with each other (in particular, so that every function has a unique representation in the BDD, even when several reduction rules apply), improving BDD algorithms to exploit the new rules, and finally implementing those algorithms efficiently in a software library.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.