基于布尔可满足性的精确逻辑综合综述

逻辑综合是电子设计自动化(EDA)的重要步骤，随着算力逐渐提升和新的计算范式不断涌现，传统基于全局启发式算法的逻辑综合面临新的挑战。启发式算法面临的主要问题是得到一个次优解，随着算力的提升，逻辑优化越来越追求精确解而不满足于次优解。该文首先简述逻辑函数表达方法和布尔可满足性(SAT)问题；其次针对精确综合的算法、编码等方面介绍了在布尔逻辑网络的面积优化和深度优化方面的精确综合研究进展；最后对精确综合的未来发展趋势进行讨论。

Survey on Exact Logic Synthesis Based on Boolean SATisfiability

Logic synthesis is a critical step in the Electronic Design Automation(EDA). Traditional global heuristic-based logic synthesis has many challenges as computing power keeps increasing and new computing paradigms emerge. There is a problem with heuristic algorithm in a suboptimal solution. As computing power improving, logic optimization is increasingly pursuing exact solutions rather than suboptimal solutions. First, the logic representations and the Boolean SATisfiability(SAT) problem are briefly described. Then, the research progress of exact synthesis in area optimization and depth optimization of Boolean logic network at two aspects, exact synthesis algorithm and encoding, are introduced. Finally, the future trends in exact synthesis are discussed.