SI2 - SSE: A Next-Generation Decision Diagram Library

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

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.