ReConcept Lab
English 中文
图谱连接

草稿

电路可满足性

判断是否存在某个布尔赋值让电路输出 1，并理解一个赋值为什么是可高效检查的证书。

concept intermediate complexityalgorithmsnp-hardnesssatisfiabilitycircuits

从点亮一盏灯开始

想象一个布尔控制电路（Boolean circuit）。它有四个输入开关 x1、x2、x3、x4。每个开关只能是 0 或 1。逻辑门（gate）如 AND、OR、NOT 会组合这些 bit，最后一条输出线 z 控制一盏灯。

判定问题（decision problem）是：

是否存在某个开关设置，让 z = 1？

电路问题问：是否有某个开关设置能点亮灯输入是开关，逻辑门执行布尔规则，导线把 bit 向前传，z=1 表示输出灯亮。
开关 = 输入 bit1 AND 0 = 01 OR 0 = 1NOT 0 = 1灯亮表示输出 1
x11x20x31x40NOTn1=1ANDg1=1ORg2=1ANDg3=1ANDg4=0ORz=11

本页始终使用同一个固定电路：

n1 = NOT x2
g1 = x1 AND n1
g2 = x3 OR x4
g3 = g1 AND g2
g4 = x2 AND x4
z  = g3 OR g4

赋值字符串按位置读取：1010 表示 x1=1、x2=0、x3=1、x4=0。

第一个朴素想法：试完所有行

最直接的方法是列出每个赋值，并在每一行上计算电路输出。

朴素搜索表

四输入电路有 16 个格式正确的行。表格展示其中一些代表行。

2^4 = 16
1010 -> z=1通过 g1 AND g2 满足

x1=1 且 x2=0 让 g1=1；x3=1 让 g2=1。

一个拒绝行只说明这一行失败，不说明整个判定问题是 No。

x11x20x31x40NOTn1=1ANDg1=1ORg2=1ANDg3=1ANDg4=0ORz=11

四个输入只有 16 行，所以暴力搜索看起来还可以接受。但这张表不是证书。它是求解器盲目搜索的空间。

贯穿全页的固定赋值行格式错误例子不放入穷举搜索表，而放在验证器和练习中。
1010 -> z=1通过 g1 AND g2 满足

x1=1 且 x2=0 让 g1=1；x3=1 让 g2=1。

0101 -> z=1通过 x2 AND x4 满足

x2=1 且 x4=1 让 g4=1，因此 z=1。

0000 -> z=0拒绝这一行，不是 No 证明

这一行失败，但其他行仍可能点亮电路。

痛点：每加一个输入就翻倍

每增加一个输入，候选行数都会翻倍：

number of assignments=2n.\text{number of assignments} = 2^n.

像 0000 这样的失败行，只能证明 0000 失败。它不能证明不存在满足行。

每增加一个输入，搜索表翻倍

检查一行只沿电路走一次；盲目搜索可能要对每一行重复检查。

原因: 搜索按翻倍增长；检查一行只沿电路走一次
赋值数量16

暴力表中的所有行

一次证书检查O(|C| + n)

检查 bit，计算逻辑门，读取 z

本例搜索16 checks for this fixture

同样增长形状，输入更大的思想实验

翻倍快照
n2^n一次检查标签
416O(|C| + n)
8256O(|C| + n)
124,096O(|C| + n)
201,048,576O(|C| + n)
301,073,741,824O(|C| + n)

核心发明：一行可以成为证书

现在把两件事分开：

  • 搜索（search）：问是否存在某个满足行。
  • 验证（verification）：接收一行候选赋值并检查它。

如果有人交给我们 1010，我们不需要再次搜索整张表。验证器（verifier）先检查它是否给每个输入一位，再按顺序计算逻辑门，最后看 z 是否为 1。

存在性搜索变成一次证书检查问题问是否存在某一行。证书是一行被声称的见证，不是自动找到它的捷径。
0000000100100011010001010110011110001001101010111100110111101111
->
被选中的证书: 1010只检查这一行

如果它让 z=1，则实例是 Yes。如果它失败，只说明这个证书失败。

证书（certificate）是一条被声称的见证。它成功时可以证明 Yes 答案，但它本身不是“找到自己”的方法。

验证器追踪：检查一个候选赋值

验证器先检查证书格式，再按拓扑顺序计算逻辑门，最后读取 z。

accept
1 / 8
验证通过赋值为每个输入提供一位

已存储的值逐步增加：每个新的门值都在其输入已知之后加入。

此步之后存储的值
x1=1x2=0x3=1x4=0
x11x20x31x40NOTn1=?ANDg1=?ORg2=?ANDg3=?ANDg4=?ORz=??
标准追踪顺序
步骤工作状态
验证通过赋值为每个输入提供一位当前
n1: NOTx2=0 -> n1=1等待
g1: ANDx1=1, n1=1 -> g1=1等待
g2: ORx3=1, x4=0 -> g2=1等待
g3: ANDg1=1, g2=1 -> g3=1等待
g4: ANDx2=0, x4=0 -> g4=0等待
z: ORg3=1, g4=0 -> z=1等待
读取最终输出最终输出 z 为 1，因此验证器接受等待

Circuit-SAT 的形式化定义

布尔电路是一个有限的有向无环网络，由输入 bit、逻辑门和导线组成。满足赋值（satisfying assignment）是让输出门等于 1 的赋值。

令 $C$ 表示一个有 $n$ 个输入变量的布尔电路，$a \in \{0,1\}^n$ 表示一个赋值，$C(a)$ 表示该赋值下的电路输出。

C∈Circuit-SAT⟺∃a∈{0,1}n such that C(a)=1.C \in \text{Circuit-SAT} \quad\Longleftrightarrow\quad \exists a \in \{0,1\}^n \text{ such that } C(a)=1.

直观地说：如果至少有一种输入设置能点亮输出灯，这个电路就是可满足的。

形式化判定语言看过具体电路后，符号 C 表示任意有 n 个输入和一个输出的布尔电路。
C

一个有限的有向无环布尔电路

a in {0,1}^n

每个输入对应一位

C(a) = 1

输出灯被点亮

验证器实现草图

验证器的职责比求解器窄：

function verifyCircuitSat(C, certificate) {
  if (!hasOneBitPerInput(C, certificate)) return false;

  const values = readInputBits(C, certificate);
  for (const gate of gatesInTopologicalOrder(C)) {
    values[gate.id] = applyBooleanGate(gate, values);
  }
  return values[C.output] === 1;
}

对格式正确的赋值：

verify(C,a)=1⟺C(a)=1.\text{verify}(C,a)=1 \quad\Longleftrightarrow\quad C(a)=1.

像 101 或 1020 这样的格式错误字符串，会在逻辑门计算前被拒绝，所以不把它们当作有意义的电路运行。

验证器实现追踪具体实现先存输入 bit，再按固定顺序存逻辑门输出。
步骤读取输入存储输出
n1 = NOTx2=0n1=1
g1 = ANDx1=1, n1=1g1=1
g2 = ORx3=1, x4=0g2=1
g3 = ANDg1=1, g2=1g3=1
g4 = ANDx2=0, x4=0g4=0
z = ORg3=1, g4=0z=1
读取 zz=1accept

逻辑门顺序不变量

电路没有环，所以可以按拓扑顺序（topological order）计算：

validation -> n1 -> g1 -> g2 -> g3 -> g4 -> z -> read final output。

不变量（invariant）是：

每计算完一个逻辑门，已经存储的每个值都等于该输入或逻辑门在当前赋值下的真实布尔值。

逻辑门顺序不变量当计算某个逻辑门时，它读取的每条线都已经有了正确布尔值。
n1x2 -> 1
g1x1 + n1 -> 1
g2x3 + x4 -> 1
g3g1 + g2 -> 1
g4x2 + x4 -> 0
zg3 + g4 -> 1

这就是验证器可以很简单的原因：它不会猜测缺失的线值，只读取已经计算好的依赖。

复杂度

证书每个输入只有一位：

∣a∣=n.|a| = n.

一次验证会检查赋值、计算逻辑门、沿导线读取依赖、最后读取输出：

one check=O(∣C∣+n).\text{one check} = O(|C| + n).

盲目搜索可能要对每个赋值都重复一次检查：

brute force search=O(2n⋅∣C∣).\text{brute force search} = O(2^n \cdot |C|).
成本堆栈在本例中，|C| 包含 4 个输入、6 个逻辑门和 11 条导线。验证器以常数门成本近似触碰每个部分一次。
检查证书n = 4

每个输入一位

计算逻辑门6 个逻辑门

拓扑顺序

沿导线读取11 条导线

依赖值已经已知

这证明了 Circuit-SAT in NP：Yes 实例有多项式大小证书，而且验证器在多项式时间内运行。

主张边界

Circuit-SAT 还有一个著名角色：根据 Cook-Levin 定理，它是 NP-hard。本节点只命名这个定理，并预告为什么 Circuit-SAT 会成为后续归约的源问题。

这个小电路、被高亮的满足行、验证器追踪，都没有证明 NP-hardness。它们只证明成员关系这一侧：证书可以被高效检查。

主张边界账本把成员关系和困难性分开。
主张处理方式原因
Circuit-SAT 属于 NP本页证明赋值长度为 n；验证器运行时间为 O(|C| + n)
Circuit-SAT 是 NP-hard本页只命名Cook-Levin 定理预告；本页不展开证明
小例子证明困难性错误小例子展示检查，不展示全称归约

常见混淆

常见混淆

每个修正都把搜索、检查和困难性主张分开。

`0000` 输出 0，所以也许电路不可满足。

修正： 失败行只排除这个赋值。No 证明需要排除所有行。

这个小追踪证明了 Circuit-SAT 是 NP-hard。

验证器会自动找到满足赋值。

太短或含非 bit 的字符串也可以送进逻辑门。

图谱连接

p-vs-np 提供证书和验证器的语言。np-hardness 提供“已知源问题可以启动后续归约链”的思想。

Circuit-SAT 是一般定义之后的第一个具体源问题。后续节点可以把 Circuit-SAT 转向 SAT 形式，但这些节点在真正存在前不会成为图谱链接。

局部图谱位置真实图谱只连接已经存在的节点。未来的 SAT 归约仅以淡化预告显示。
P 与 NP

证书与验证器

->NP-Hardness

源问题角色

->电路可满足性

第一个具体源

->SAT

后续转换，暂不链接

练习

练习边界

区分行、格式错误证书，以及“已证明/只命名”的主张边界。

验证器应如何处理证书 1010？

选择一个答案来检查。

0000 证明了什么？

选择一个答案来检查。

应该如何处理 101？

选择一个答案来检查。

1020 的问题是什么？

选择一个答案来检查。

本页真正证明了哪条主张？

选择一个答案来检查。
  1. 在赋值 1010 中，哪个逻辑门最先让它看起来有希望？
  2. 为什么 0000 不能证明整个电路不可满足？
  3. 为什么 101 应该在任何逻辑门计算前停止？
  4. 本页证明了哪条主张：Circuit-SAT in NP、Circuit-SAT is NP-hard，还是二者都证明？

图谱连接 : 电路可满足性