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

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

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.