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

点击翻译按钮获取中文摘要

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.