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

SHF：中：提高决策图的效率和适用性

• 批准号: 2212142
• 负责人: Andrew Miner
• 金额: $ 70万
• 依托单位: Iowa State University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2022
• 资助国家: 美国
• 起止时间: 2022-10-01 至 2025-09-30
• 项目状态: 未结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=2212142&HistoricalAwards=false
• 关键词: SHF; Medium; Improving; Efficiency; Applicability

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.

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

项目成果

Research Directions in Decision Diagram Technology

决策图技术研究方向

• 发表时间: 2023
• 期刊: IEEE John Vincent Atanasoff Symposium on Modern Computing
• 作者: Ciardo, Gianfranco;Miner, Andrew S.
• 通讯作者: Miner, Andrew S.

Computing under-approximations of multivalued decision diagrams

计算多值决策图的欠近似值

• 发表时间: 2023
• 期刊: Application and Theory of Petri Nets and Concurrency
• 作者: Hosseini, Seyedehzahra;Ciardo, Gianfranco
• 通讯作者: Ciardo, Gianfranco