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.