2. 布尔可满足性问题（SAT）：SAT问题的定义、CNF范式、DPLL算法简介

各位同学，今天我们聊聊SAT。嗯，布尔可满足性问题，听起来挺唬人的。但说白了，它就是问一个问题：给定一堆布尔变量和它们之间的逻辑关系，能不能找到一组赋值，让整个表达式为真？

我在做覆盖率分析的时候，经常遇到这种情况。约束条件写了一大堆，仿真跑不动了。这时候我就会想：这些约束到底有没有解？是不是自相矛盾了？SAT求解器就是干这个的。

SAT问题的标准定义是这样的：

举个例子。公式 F = (x₁ ∨ x₂) ∧ (¬x₁ ∨ x₃)。你试试看，x₁=1, x₂=0, x₃=1 就能让F为真。所以这个公式是SAT的。

但 F = x₁ ∧ ¬x₁ 呢？这明显不可能同时成立。这就是UNSAT。

核心要点：SAT问题的本质就是判断约束系统是否有解。在EDA中，我们经常把覆盖率约束、时序约束、功能约束都转化成SAT问题来求解。

你可能会问：实际中的公式那么复杂，怎么统一处理？

答案是：标准化。业界通用的标准形式叫CNF，也就是合取范式。

CNF长这样：

(a ∨ ¬b ∨ c) ∧ (¬a ∨ d) ∧ (b ∨ ¬c ∨ ¬d)

每个括号叫一个子句（clause），子句之间用AND连接。子句内部是OR连接的变量或变量的否定。每个变量或它的否定叫文字（literal）。

为什么用CNF？我个人习惯是：

我记得有一次，一个同事把复杂的时序约束直接扔给SAT求解器，结果跑了三天没出结果。我一看，约束没转成CNF，求解器根本不认。嗯，这种坑我踩过。

小技巧：任何布尔公式都可以转化为CNF。常用的方法有Tseitin变换，它通过引入新变量来避免指数爆炸。我在项目中经常用这个方法处理复杂的覆盖率约束。

好了，有了CNF，怎么求解？最经典的算法就是DPLL。名字取自四位发明者的首字母：Davis、Putnam、Logemann、Loveland。

DPLL的核心思想其实很简单，就三步：

说白了，就是深度优先搜索 + 剪枝。但DPLL聪明的地方在于推导这一步。

举个例子。假设CNF中有个子句 (a ∨ b)，你给a赋了0。那这个子句就变成了 (0 ∨ b)，也就是必须b=1才能满足。这叫单元传播（Unit Propagation）。

如果某个变量只以同一种形式出现（全是正或全是负），那可以直接赋值。这叫纯文字规则（Pure Literal Rule）。

下面我用SVG画个流程图，帮你理清DPLL的执行逻辑：

这个图你看懂了吗？从上往下走，决策→推导→检查矛盾。没矛盾就继续，有矛盾就回溯。直到所有变量都赋值了，那就是SAT。如果所有分支都试过了还是不行，那就是UNSAT。

注意：DPLL在最坏情况下是指数复杂度的。但实际中，通过好的决策启发式（比如VSIDS）和冲突驱动子句学习（CDCL），现代SAT求解器可以处理百万变量级别的问题。

我曾经在一个覆盖率分析项目中，遇到一个诡异的bug。约束条件明明看起来没问题，但仿真就是覆盖不到某些分支。

后来我把约束转成CNF，用DPLL跑了一遍。你猜怎么着？约束本身是矛盾的！某些覆盖率事件永远不可能同时发生。嗯，这就是典型的约束过约束问题。

从那以后，我养成了一个习惯：在写覆盖率约束之前，先用SAT求解器检查一下约束的可满足性。这能省下大量调试时间。

实用建议：如果你刚开始接触SAT求解，我推荐从MiniSAT开始。代码量不大，注释清晰，是学习DPLL和CDCL的绝佳教材。我自己当年就是啃完MiniSAT源码后，对SAT的理解上了一个台阶。

好了，这一章就到这里。SAT是形式化验证的基石，理解它对你后面学习SMT、模型检验都很有帮助。记住：约束可满足性检查，是覆盖率分析的第一步，也是最关键的一步。