G中国科学院研究员蔡少伟：S 算法

雷峰网按：2021 年 12 月 9 日-2021 年 12 月 11 日，2021 第六届全球人工智能大会（GAIR 2021）于深圳正式召开。历经五年，见证数次潮水的转向，成为目前为止粤港澳大湾区人工智能领域规模最大、规格最高的学术、工业和投资领域跨界盛会。
【 G中国科学院研究员蔡少伟：S 算法】在大会第二天举办的“集成电路高峰论坛：国产高端芯片之路”上，汇聚来自学术界、产业界和投资界的 15 位大咖，共同探讨了国产高端芯片的实力以及 RISC-V 带给中国芯片的机会。
EDA是中国芯片产业发展的卡脖子技术，求解器又是EDA的基础引擎，解决了基础技术挑战才能支撑整个产业的快速发展——基于此，中国科学院软件研究所研究员蔡少伟主要从自己的研究角度谈到了 EDA 的发展。
蔡少伟的演讲主要涵盖三个方面，一是 EDA 和 SAT 求解器的关系；二是举例说明 SAT 求解器在 EDA 当中的应用；三是分享其团队在 SAT 求解器方面的进展。
蔡少伟表示，EDA 集成电路设计自动化软件，整条链很长，而不是单个的软件。在 EDA 软件中，其底层需要一些计算引擎，而主要的计算引擎就是 SAT 求解器。
在 EDA 各个环节中，包括逻辑综合、物理实现，以及中间的验证、仿真测试都会用到 SAT 求解器。
目前，蔡少伟团队的 SAT 求解器已经用于集成电路验证的实际场景，在 1 小时内可求解出一些近 2 亿子句规模的算例。
以下是蔡少伟在GAIR 2021 上的演讲内容，雷峰网进行不改变原意的编辑整理：
今天的汇报分为3个部分：一是 EDA 和 SAT 求解器的关系；二是举几个例子说明 SAT 求解器在 EDA 中的应用；三是介绍团队在 SAT 求解器方面的进展。
EDA 的全称是 ElectronicDesignAutomation，是指集成电路的设计自动化软件，用这样一套软件自动设计集成电路，一般都称 EDA 为芯片之母，是整个半导体的最上游、支撑芯片乃至整个信息产业的共性基础技术。
EDA集成电路设计自动化软件不是单个的软件，整个条链很长，我们可以把 EDA 软件当成硬件编译器，用硬件描述语言写出芯片的需求，通过 EDA 软件可以帮助我们自动的设计出芯片集成电路的版图。
EDA 软件里面，底层需要一些计算引擎，而主要的计算引擎就是 SAT 求解器，在 EDA 的各个环节里，包括逻辑综合、物理实现，以及中间的验证、仿真测试其实都要用到 SAT 求解器。
比如，以逻辑综合为例，在逻辑综合的历史上，SAT 求解器一直扮演非常重要的角色，尤其是在逻辑综合的发展史上最后一个阶段，优化和表示都要极大依赖 SAT 求解器。
在电路的形式化验证方面，形式化验证工具主要有两类：模型检测工具和等价性验证工具。模型检测主要是用来证明一个电路是否满足某个属性，而等价性验证用来证明两个电路是否等价。
以模型检测技术的发展为例，在这个发展历史阶段中，从 2000 年之后开始的模型检测技术基本都是基于 SAT 求解器来开发的。
通常情况下，计算机解决问题的时候有两类思路：一是把问题清楚地用数学语言描述出来，再设计算法求解，这是约束求解的思路，典型场景包括定理证明等。二是机器学习，用户提供例子，计算机解决问题，比如，各种模式识别的任务比较适用于机器学习。对于需要严格证明的场景，则需要约束求解来解决。
SAT 的全称是布尔可满足性问题，这个问题的描述非常简单，即给定一个布尔公式或称为命题逻辑公式，也即用与或非等逻辑连接词连接起来的公式，判断是否能给公式里的变量赋值使得公式为真。如果存在这样的赋值，就说这个公式是可满足的，否则就是不可满足的。