电路可满足性问题

电路把共享子表达式保留下来，是比公式更紧凑的约束语言。SAT 求解器必须为输入变量选值，让信号沿 DAG 传播后把输出门推到 $1$；内部门值并非独立猜测，而由前驱唯一决定。共享既能缩短输入描述，也会让一个选择同时影响许多后继，这正是把 Circuit-SAT 简单展开成公式可能付出指数代价的原因。

穷举基线清楚而残酷：依次检查全部 $2^n$ 个赋值，每次用 $O(s)$ 时间求值，总时间 $O(2^{n}s)$。改进可以来自门类限制、结构宽度、变量分割或批量求值，但比较算法时必须说明是把指数底数降到 $2-\epsilon$，还是只节省多项式因子；两者对细粒度假设和下界推论的意义完全不同。

考虑

按字典序检查：$000$ 与 $001$ 的第一括号都为 $0$，故拒绝；到 $010$ 时，第一括号为 $1$，第二括号因 $\mathrm{\neg }{x}_1=1$ 也为 $1$，所以 $010$ 是可验证见证，搜索可以停止。若把每个内部门写成拓扑表，验证者只需计算一次 NOT、两次 OR 和一次 AND，而不需再次搜索内部状态。

Circuit-SAT 的 NP 完全性不说明现有实例都接近 $2^n$ 困难，也不排除某个受限电路类拥有快速算法。参数化上，$s$ 可能远大于 $n$；一个写成 $2^n\mathrm{poly}(s)$ 的算法对门数仍是多项式，但若电路编码允许指数 bit 权重，“$\mathrm{poly}(s)$”就没有覆盖完整输入长度。多输出电路可加一个 OR 或指定某个输出，约定需要显式转换。

SETH公理库强指数时间假设 SETHStrong Exponential Time Hypothesis · SETH假设随着子句宽度增长，k-SAT 的最优指数底数不能被某个统一小于 2 的常数界定。 给出一条安全的单向边界：若一般 Circuit-SAT 能对所有多项式大小电路在 $O((2-\epsilon {)}^n\mathrm{poly}(s))$ 时间求解，那么同一算法作用于 $k$-CNF 电路会否定 SETH。反向把 SETH 写成所有 Circuit-SAT 界的等价陈述则需要限制电路大小与归约膨胀；SETH 也不排除 $2^n/n^{100}$ 这类未改变指数底数的改进。

Circuit-SAT 是 Cook–Levin 理论、逻辑综合和自动验证的共同核心。把时间有界计算展开为电路，再询问是否存在满足输入，可把非确定计算统一编码成组合搜索；实际 SAT 求解还会把门转成 CNF 并引入辅助变量，转换保持等可满足性而非逐赋值使用同一变量表。

更深的联系是“算法产生下界”。Williams 证明，对具有合适闭包性质的电路类，若其 Circuit-SAT 能以足够非平凡的方式快于穷举，就可结合时间层级定理推出 $NEXP$ 等类不具有该类小电路；ACC⁰ 是代表性成功案例。精确节省、可处理规模和闭包条件都是定理假设，不是任意小优化都自动给出下界。

这条算法路线与自然证明障碍公理库自然证明障碍Natural proofs barrier · Razborov-Rudich natural proofs在强伪随机函数假设下排除同时具备构造性、大性和有用性的一般电路下界性质。互为对照：前者利用求解受限电路的算法和层级矛盾，后者说明在强 PRF 假设下某类大而可构造的真值表性质不能证明一般下界。二者共同界定当前一般电路下界研究的可行与受阻方向。