SAT 求解器 在EDA的各个环节都有广泛应用，比如：逻辑综合、物理实现、中间验证、仿真测试。
电路的形式化验证方面，形式化验证工具主要有两类：模型检测工具和等价性验证工具。
模型检测工具主要用于证明一个电路是否满足某个属性，而等价性验证用来证明两个电路是否等价。
计算机解决问题的时候有两类思路：
一是：把问题清楚的用数学语言描述出来，再设计算法求解，这是约束求解的思路，典型场景包括定理证明等等。
二是：机器学习，用户提供例子，计算机解决问题，比如各种模式识别。
对于需要严格证明的场景，更适合使用约束求解来解决。
SAT（布尔可满足性问题），给定一个布尔公式或者命题逻辑公式，即 用与、或、非 等逻辑联接起来的公式，判断是否能给公式里的变量赋值使得公式为真。
如果存在这样的赋值，则说明这个公式是可满足的，否则就是不可满足的。
SAT涉及到的基本概念包括：变量，文字、子句（子句是文字的析取）、合取范式（简称CNF，子句的合取，即子句集合）。SAT的求解一般采用合取范式输入，也有针对电路的SAT问题。
注意：析取范式(j简称DNF，子句的析取)的逻辑并不是SAT问题，而是K- DNF问题
合取可称为逻辑与，析取则可称为逻辑或，用符号∧表示 。符号∧读作“并且”。
SAT在EDA中的典型应用举例
Step1 将电路转换为CNF（SAT可接受的输入形式）
比如 与 门电路
C=A*B
转为CNF 为
(非A V 非B V C) ∧ (A V 非C) ∧ (B V 非C)
可以将其翻译成一条 SAT 公式，如果这条公式用 SAT 求解器来判定，它是可满足的，就意味着它存在一个反例，并且可以对应地将这条反例构造出来。如果这个公式是不可满足的，就是说不存在反例，这个属性是被验证满足的了。
如图，假设 d 这条线断了，它为 0，要找到一个输入使得正常设计的情况下输出和在另一边输出不一样，从而发现出现断路的情况。
由此，要产生一个满足两个条件的测试向量：一是错误的激活，二是错误要传播，将两个条件编码为一个 CNF 公式，合起来其实也是 SAT 求解问题。
SAT 求解器在 EDA 中如此重要，那么，它目前做得怎么样？
SAT 是一个逻辑问题，很容易会采用逻辑推理的方法思考，比如说归结原理。但把它看作在搜索空间找赋值，判断它是否存在合法的解，因此搜索的方法也可行。
SAT 求解方法可以分为两类：完备算法和不完备算法。完备算法是指算法只要给足时间，肯定会产生正确答案，Yes or No，但这个时间在理论上没有保证；不完备算法是指争取短时间内找到解。
参照：中国科学院研究员蔡少伟：SAT 求解器 EDA 基础引擎｜GAIR 2021 (baidu.com)
标签：EDA,求解,公式,算法,集成电路,应用,子句,SAT From： https://www.cnblogs.com/oceaning/p/17065244.html