Graphical Structures for Coding and Verification

图结构上的算法在通信技术和形式验证中起着核心作用。 最小网格是纠错码的图形表示，它已经成为理解和操作所有类型代码的统一框架。 有序二元决策图及其变体是基于图的数据结构，用于表示布尔函数，这些布尔函数已广泛用于一系列问题的形式验证，包括电路检查，逻辑合成和测试生成。 这个项目建立在最近建立的代码格和二进制决策图之间的密切对应关系，并调查这些以前不同的领域之间的思想转移。 这两种图形方法所面临的基本挑战是相同的：设计技术来对抗图形大小的指数爆炸。 这项研究是跨学科的，可以预期有广泛的应用，无论是在编码和验证，以及人工智能，数据库搜索和组合优化等领域。

Algorithms on graphical structures play a central role in both communications technology and formal verification. Minimal trellises are graphical representations of error-correcting codes that have emerged as a unifying framework for understanding and manipulating codes of all types. Ordered binary decision diagrams and their variants are graph-based data structures for representing Boolean functions that have found widespread use in formal verification for a range of problems, including circuit checking, logic synthesis and test generation. This project builds on the close correspondence that has recently been established between the code trellis and binary decision diagram, and investigates the transfer of ideas between these previously disparate fields. The fundamental challenge that confronts both uses of graphical methods is the same: devise techniques to combat the exponential blowup in the size of the graph. The research is interdisciplinary, and can be expected to have a broad range of application, both within coding and verification, as well as to such areas as artificial intelligence, database search, and combinatorial optimization.