草稿
从 Circuit-SAT 到 SAT 的归约
通过为每个门设置辅助变量，并加入局部门约束，把电路可满足性实例翻译为 SAT 实例。
这是从电路视图到公式视图的第一座桥：
- 源问题：Circuit-SAT
- 目标问题：SAT
- 承诺：构造后保持 Yes/No 回答不变，且是多项式时间构造
4 个输入，6 个门，1 个输出
n1 = NOT x2 ; g1 = x1 AND n1 ; g2 = x3 OR x4 ; g3 = g1 AND g2 ; g4 = x2 AND x4 ; z = g3 OR g4可满足当且仅当 z 能取 1
Φ_C = z ∧ (∧_{g in Gates(C)} emit(g))，每个 emit(g) 仅由 AND/OR/NOT 构成。| 赋值 | C(a) | 去 z 的合取 | 最终 Φ_C(â) | 注解 |
|---|---|---|---|---|
| 1010 | 1 | 1 | 1 | 该赋值下电路输出与归约后的公式输出一致。 |
| 0101 | 1 | 1 | 1 | 该赋值下电路输出与归约后的公式输出一致。 |
| 0000 | 0 | 1 | 0 | 所有局部门约束为真，但 AND z 会继续拒绝。 |
共享的源电路与 circuit-sat 页面一致：
赋值字符串按 x1 x2 x3 x4 排列。例如 1010 表示：
引子问题：同样的“存在”问题，不同对象
Circuit-SAT 问是否存在输入让 z=1，SAT 问是否存在赋值让某个公式为真。
两者都在问“是否有满足的赋值”，但目标对象不同：一个是门电路，一个是公式。
所以需要一个显式翻译，保证答案保真，而不是靠直觉猜测。
朴素尝试：展开成一个大公式
一个直接想法是把每个门表达式一直替换，直到只剩输入。
n1 = NOT x2
g1 = (x1 AND NOT x2)
g2 = (x3 OR x4)
g3 = ((x1 AND NOT x2) AND (x3 OR x4))
g4 = (x2 AND x4)
z = (((x1 AND NOT x2) AND (x3 OR x4)) OR (x2 AND x4))
z = (((x1 AND NOT x2) AND (x3 OR x4)) OR (x2 AND x4))该方法保持语义，但会反复复制共享子表达式。
语义上是对的，但这会复制共享子电路，难以控制规模。
为什么展开不是正确的一般解
Fan-out 本来是电路复用的优势；全量展开会把共享逻辑复制多份。
h=(a OR b); p=h AND c; q=h AND d; z=p OR q共享子表达式 h 只使用一次z=((a OR b) AND c) OR ((a OR b) AND d)内联后 h 被使用两次因此我们不直接生成完整展开公式。
核心发明：门变量 + 局部门约束
给每个非输入节点加一个辅助变量，用它原来的门名命名：
n1、g1、g2、g3、g4、z。
每个门发出一条局部约束，强制该辅助变量等于门表达式值。 页面里我们把两个层次分开：
blueprint（阅读用）用 <-> 写法；
emit（真正 SAT 实例）只使用 AND/OR/NOT。
蓝图: g <-> (u AND v)
实际输出: (NOT g OR (u AND v)) AND (NOT (u AND v) OR g)
两个输入、一个辅助变量、常数规模约束。
| 输入 | 输出 |
|---|---|
| 00 | 0 |
| 01 | 0 |
| 10 | 0 |
| 11 | 1 |
蓝图: g <-> (u OR v)
实际输出: (NOT g OR (u OR v)) AND (NOT (u OR v) OR g)
结构同 AND，只是 RHS 运算符改为 OR。
| 输入 | 输出 |
|---|---|
| 00 | 0 |
| 01 | 1 |
| 10 | 1 |
| 11 | 1 |
蓝图: g <-> NOT u
实际输出: (NOT g OR NOT u) AND (u OR g)
一元形式只用一个输入，编码风格一致。
| 输入 | 输出 |
|---|---|
| 0 | 1 |
| 1 | 0 |
输入变量 x1..x4 是问题变量（与 Circuit-SAT 输入同名）。
辅助变量 n1, g1, g2, g3, g4, z 对应电路的门输出。
形式化构造
对每个门 g：
其中 rhs 是该门局部右侧表达式（AND/OR/NOT）。
归约公式的构造顺序依赖电路无环性：每个门只依赖输入节点或更早已定义的门。
归约后的公式是：
Φ_C = z ∧ (∧_{g in Gates(C)} emit(g))，每个 emit(g) 仅由 AND/OR/NOT 构成。
emit(n1) = ((NOT n1 OR NOT x2)) AND ((NOT (NOT x2) OR n1))
emit(g1) = ((NOT g1 OR (x1 AND n1))) AND ((NOT ((x1 AND n1)) OR g1))
emit(g2) = ((NOT g2 OR (x3 OR x4))) AND ((NOT ((x3 OR x4)) OR g2))
emit(g3) = ((NOT g3 OR (g1 AND g2))) AND ((NOT ((g1 AND g2)) OR g3))
emit(g4) = ((NOT g4 OR (x2 AND x4))) AND ((NOT ((x2 AND x4)) OR g4))
emit(z) = ((NOT z OR (g3 OR g4))) AND ((NOT ((g3 OR g4)) OR z))
再乘上 z
真正输出到 SAT 的是 Φ_C，它只含 AND/OR/NOT。
赋值扩展与限制
归约后的赋值域比电路多了辅助变量；反向方向会先把 SAT 赋值限制回 x1..x4。
输入行: x1=1, x2=0, x3=1, x4=0
扩展后: x1=1, x2=0, x3=1, x4=0, n1=1, g1=1, g2=1, g3=1, g4=0, z=1
限制后: x1=1, x2=0, x3=1, x4=0
输入行: x1=0, x2=1, x3=0, x4=1
扩展后: x1=0, x2=1, x3=0, x4=1, n1=0, g1=0, g2=1, g3=0, g4=1, z=1
限制后: x1=0, x2=1, x3=0, x4=1
正确性方向 1：Circuit-SAT ⇒ SAT
若某个电路赋值 a 让 C(a)=1，我们把门输出一起扩展到 (x1..x4, n1,g1,g2,g3,g4,z)。
每条局部约束都被满足，并且 z=1，所以归约后公式 Φ_C 也满足。
正确性方向 2：SAT ⇒ Circuit-SAT
若某个 SAT 赋值 b 满足 Φ_C，每条约束都迫使辅助变量等于对应门的真实结果。
把它限制到 b|inputs| 后即可按拓扑顺序重算电路，得到 z=1，于是 C(b|inputs|)=1。
这是为什么双向都要写清楚。
正确性支撑（正向与反向）
1010: C(a)=1 -> Φ_C(â)=1
b=1010: Φ_C(b)=1 => C(b|inputs|)=1
| 赋值 | C(a) | 去 z 的合取 | 最终 Φ_C(â) |
|---|---|---|---|
| 1010 | 1 | 1 | 1 |
| 0101 | 1 | 1 | 1 |
b|inputs| 中的输入: x1=1, x2=0, x3=1, x4=0
扩展后的辅助变量值: x1=1, x2=0, x3=1, x4=0, n1=1, g1=1, g2=1, g3=1, g4=0, z=1
限制后的 b|inputs|: x1=1, x2=0, x3=1, x4=0
b|inputs| 中的输入: x1=0, x2=1, x3=0, x4=1
扩展后的辅助变量值: x1=0, x2=1, x3=0, x4=1, n1=0, g1=0, g2=1, g3=0, g4=1, z=1
限制后的 b|inputs|: x1=0, x2=1, x3=0, x4=1
若某些辅助变量与门式冲突，局部约束会拒绝该赋值。
以 0000 为底的作弊示例：
x1=0, x2=0, x3=0, x4=0, n1=1, g1=1, g2=0, g3=0, g4=0, z=0
NOT g1 OR (x1 AND n1) 为假，因为 x1=0,n1=1 但 g1=1。
专门的 AND z 对照
没有最后的 AND z 时，局部门约束可能都真，但输出端是 0，会被错误接受。
| 赋值 | 门约束合取 | z | Φ_C | 说明 |
|---|---|---|---|---|
| 0000 | 1 | 0 | 0 | 只满足一致性的赋值会让所有门约束成立，但 AND z 会拒绝它。 |
主归约追踪（主演示）
这个追踪显示按拓扑顺序发射局部约束、累计前缀以及最终 AND z。
归约对某个固定赋值逐门处理，按拓扑顺序逐步发射约束。
发射 n1: n1 <-> (NOT x2) -> ((NOT n1 OR NOT x2)) AND ((NOT (NOT x2) OR n1))
该步约束真值 = 1
赋值先验必须合法，每一步只使用已存储的前置值。
输入 x1=1, x2=0, x3=1, x4=0
辅助变量 n1=1
累计 emitted 公式前缀
((NOT n1 OR NOT x2)) AND ((NOT (NOT x2) OR n1))
n1 <-> (NOT x2)
((NOT n1 OR NOT x2)) AND ((NOT (NOT x2) OR n1))
| 步骤 | 工作 | 发射值 |
|---|---|---|
| 1 | 发射 n1 | ((NOT n1 OR NOT x2)) AND ((NOT (NOT x2) OR n1)) |
| 2 | 发射 g1 | ((NOT g1 OR (x1 AND n1))) AND ((NOT ((x1 AND n1)) OR g1)) |
| 3 | 发射 g2 | ((NOT g2 OR (x3 OR x4))) AND ((NOT ((x3 OR x4)) OR g2)) |
| 4 | 发射 g3 | ((NOT g3 OR (g1 AND g2))) AND ((NOT ((g1 AND g2)) OR g3)) |
| 5 | 发射 g4 | ((NOT g4 OR (x2 AND x4))) AND ((NOT ((x2 AND x4)) OR g4)) |
| 6 | 发射 z | ((NOT z OR (g3 OR g4))) AND ((NOT ((g3 OR g4)) OR z)) |
| 7 | 断言 output 约束 | z |
实现与不变量
实现上是：每个门输出一个常数规模约束，按拓扑顺序写下，再加最终输出约束。
| 步骤 | 门 / 辅助变量 | 蓝图 | 局部约束 |
|---|---|---|---|
| 1 | n1 | n1 <-> (NOT x2) | ((NOT n1 OR NOT x2)) AND ((NOT (NOT x2) OR n1)) |
| 2 | g1 | g1 <-> (x1 AND n1) | ((NOT g1 OR (x1 AND n1))) AND ((NOT ((x1 AND n1)) OR g1)) |
| 3 | g2 | g2 <-> (x3 OR x4) | ((NOT g2 OR (x3 OR x4))) AND ((NOT ((x3 OR x4)) OR g2)) |
| 4 | g3 | g3 <-> (g1 AND g2) | ((NOT g3 OR (g1 AND g2))) AND ((NOT ((g1 AND g2)) OR g3)) |
| 5 | g4 | g4 <-> (x2 AND x4) | ((NOT g4 OR (x2 AND x4))) AND ((NOT ((x2 AND x4)) OR g4)) |
| 6 | z | z <-> (g3 OR g4) | ((NOT z OR (g3 OR g4))) AND ((NOT ((g3 OR g4)) OR z)) |
这样就能做到机械化的、一致的构造。
复杂度
设 |C| 表示该固定电路编码规模。每个非输入节点贡献一个辅助变量和一条常数规模约束，再加最终 z。
| 类型 | 数量 |
|---|---|
| 输入变量 | 4 |
| 辅助变量 | 6 |
| 门约束 | 6 |
| 最终输出约束 | 1 |
所以 |Φ_C| = O(|C|)，是线性规模；这里依赖固定门扇入假设：AND/OR 为双输入，NOT 为单输入。
该线性规模结论依赖固定扇入的假设（AND/OR 是 2 输入，NOT 是 1 输入）。
常见混淆
始终把蓝图、顺序、辅助变量角色讲清。
写 `g <-> expr` 很简洁，直接当作输出公式可以吗？
修正： 不行。`<->` 只是本地可读写法，累积的 SAT 输出必须只用 AND/OR/NOT。
每个门一致即可，不需要额外约束输出。
约束顺序随意写即可，拓扑顺序只是实现细节。
不需要辅助变量，只出现 x1..x4 即可。
图谱连接
polynomial-time-reductions 提供模板，circuit-sat 提供源实例，sat 提供目标对象。
答案保持翻译器
源问题
目标语言
本节点
练习
按归约语义分类固定示例与格式错误处理。
选择答案以检验。
选择答案以检验。
选择答案以检验。
选择答案以检验。
- 在共享赋值中，哪些行可作为归约保留答案的例子？
- 为什么
0000会被门约束接受却被AND z拒绝？ - 为什么
<->只能当蓝图，不应直接作为最终 SAT 输出语言？ - 输入变量和辅助变量分别是哪一类？
图谱连接 : 从 Circuit-SAT 到 SAT 的归约