计算布尔代数：香农展开与 SAT

TL;DR

• Shannon expansion是将Boolean function分解为一个MUX的公式。
• cofactor是“将一个变量固定为0/1后的新function”，因此该变量会在cofactor中消失。
• Boolean difference是用于计算“翻转输入x时输出是否改变？”的sensitivity function。
• ∃(existential) quantification是将“只要存在任意一个解即可”写成公式的运算，这正是SAT的核心。
• Optimization通常更难：SAT找到一个满足解即可结束，而Optimization还需要比较候选解，并证明不存在更优解；边界估计与剪枝可以减少搜索。

1. 问题意识：Karnaugh map失效的时刻

1.1 如果是40 variables，Karnaugh map就不够用了

• 2^40规模 → “即使能画出来，也无法使用”
• 结论：必须不再手工处理，而是通过data structure + operator处理Boolean function。

1.2 本文的3个目标

• decomposition（拆分）
• computation（程序可处理的表示）
• application（在EDA中直接使用的运算）

2. Shannon cofactor：“变量固定”所产生的新function

2.1 定义：cofactor是substitution

• 对于f的输入变量x
  • positive cofactor: ( f_{x} = f(x=1) )
  • negative cofactor: ( f_{~{x}} = f(x=0) )

2.2 核心要点：“它是新function，且x会消失”

• 既然将x固定为0/1，结果中就不可能再出现x。
• 若忽略这一点，后续的Boolean difference / quantification都会失去基础。

2.3 （简短示例）

• 例：( f(x,y,z) = xy+x~z+~xyz )
  • ( f(x=1) = y + \bar{z} )（可简化）
  • ( f(x=0) = yz )

3. Shannon expansion：将“Boolean function = MUX”看清后，问题就解决了

3.1 定理（Shannon expansion theorem）

对于任意f和任意变量x：
f=x⋅f(x=1)+~x⋅f(x=0)

3.2 硬件视角：Shannon expansion = 2:1 MUX

• select = x
• data1 = f(x=1)
• data0 = f(x=0)
• output就是f

📌 这里形成“分支(branch)”的直觉：

• 沿x=0分支向下时，只需看f(x=0)
• 沿x=1分支向下时，只需看f(x=1)

3.3 MUX tree = recursive decomposition

• 一个变量 → 2个分支
• 两个变量 → 4个分支
• k个变量 → 2^k个分支
• 这看起来像“枚举”，但EDA会在这里进行pruning。（后文说明）

[Figure 1] 将Shannon expansion绘制为2:1 MUX的图
[Figure 2] 展示2-variable expansion生成4个leaf的MUX tree图

4. cofactor中“运算可交换”：计算变简单的原因

4.1 非常重要的性质

• complement:
  • (~f)x=~(𝑓𝑥)
• AND/OR/XOR同样可以“先cofactor → 后运算”
  • (𝑓∧𝑔)𝑥=𝑓𝑥∧𝑔𝑥

也就是说，不是先构造大表达式再进行cofactor，
而是先进行cofactor缩小表达式，然后再计算。

5. Boolean difference：将“敏感度(sensitivity)”写成公式

5.1 定义

∂f/∂x​=f(x=1)⊕f(x=0)

5.2 含义：“翻转x时输出改变的条件”

• XOR表示“不同则为1”
• 因此，在Boolean difference为1的输入模式下：
  • 将x从0→1或1→0时，f必然改变

5.3 通过示例建立直觉

• inverter: f=~x
  • 𝑓(1)=0,𝑓(0)=1⇒∂𝑓/∂𝑥=1
  • 始终敏感
• AND: ( f=xy )
  • 𝑓(1)=𝑦,𝑓(0)=0⇒∂𝑓/∂𝑥=𝑦
  • 仅当y=1时，x的变化才影响输出
• OR: ( f=x+y )
  • 𝑓(1)=1, 𝑓(0)=𝑦 ⇒ ∂𝑓/∂𝑥=~𝑦
  • 仅当y=0时才有影响

5.4 “x对F没有逻辑影响？”的准确解释

• 这并非指“始终没有影响”。
• 而是指在特定输入条件下可能没有影响。
• Boolean difference恰好能提取出该条件。

[Figure 3] 展示AND/OR中Boolean difference为何分别为y / ȳ的门电路图

6. Quantification：以“消去变量”为目的的运算

6.1 existential quantification (∃)：“只要有任意一个解即可”

∃xf=f(x=0)∨f(x=1)

• 含义：当其他输入固定时，能否恰当选择x使f=1？

6.2 universal quantification (∀)：“必须在所有情况下成立”

∀xf=f(x=0)∧f(x=1)

• 含义：无论x为何值，f是否始终为1？

6.3 你所说的句子与1:1对应

“无需全部枚举，只要找到任意一个解即可”

这正是：

∃ quantification

• 以及SAT的核心形式：∃X:F(X)=1

7. SAT vs Optimization：为什么“优化”更困难

7.1 SAT：“找到一个即可结束”

• 只要存在满足条件的解即可结束
• 分支搜索中只要有一个满足条件，即可终止（pruning）

7.2 Optimization：“比较才是本质”

• 若要确认当前解是否最优，通常还需要搜索其他候选分支
  • 边界估计与剪枝可以提前排除部分分支
• 因此，EDA优化在结构上更困难（可引出NP-hard的讨论）

[Figure 4] 展示SAT在第一个满足条件时stop、Optimization则继续搜索的树图

自然衔接至下一讲：Tautology与URP

8.1 tautology：“是否始终为1？”

• ​f≡1?
• 核心思想：f是tautology ⇔ f(x=0)和f(x=1)也都是tautology

8.2 URP的直觉

• 通过Shannon cofactor进行分解（分支）
• 若满足unate等条件，则可在中途立即终止（强pruning）
• 最终它不是“枚举”，而是“快速丢弃应丢弃项的算法”

本文必须掌握的5项

1. cofactor是substitution，且相应变量会在结果function中消失
2. Shannon expansion既是公式，同时也是2:1 MUX模型
3. Boolean difference是给出“x变化影响输出的条件”的function
4. ∃ quantification通过OR实现“只要有一个即可”
5. SAT有一个即可结束，Optimization因比较而耗时更长