专题 · FULL STORY

OpenAI SAT 求解器与 ETH 之争

OpenAI 疑似违反指数时间假设的 SAT 求解器在理论计算机科学界引发热议。Duke 教授 minilek 与 Ryan Williams 先后辨析 ETH 是否站得住脚，Williams 进一步指出该算法属于「split and list」方法，争议持续发酵。

2026-10-28 ~ 2026-10-30 · 2 集 · 9 条

第 1 集 · minilek 与 Ryan Williams 辨析 ETH 站得住吗(2026-10-28,7 条)

10 月 28 日至 29 日，Duke 教授 minilek（Donald Knuth 传记作者、ACM CSSI 创始人）与理论计算机科学家 Ryan Williams 在 X 上围绕指数时间假设（ETH）展开多轮技术讨论，起因是 Williams 反驳强指数时间假设（SETH）的新工作引发的追问。讨论的共同结论是：ETH 目前仍站得住，但需要澄清其真实适用边界。

已确认

  • minilek 的核心疑问：除了「聪明人一直没找到更快算法」这一经验事实外，历史上是否有实质性理由相信 ETH 应当成立。
  • Williams 承认，一系列论文已把 SAT 的指数底数从 2^n 压到更小的 c^n（帖子提及平凡 1.913^n 算法），因此「不存在比蛮力更好的算法」这一前提其实早已不成立，这也是他当年对 ETH 持怀疑态度的原因之一。
  • 针对 minilek 追问已知最优 SAT 算法（如 PPSZ 类 (2-ε)^n 亚指数算法）是否落入某条下界约束：Williams 答复称，已知算法的扩展已知仍遵守 ETH；指数时间下界（如排除 2^{o(n)} 算法）只对受限算法类成立，例如归结（resolution）类方法——这类方法刻画了现代 SAT 求解器的主要行为。
  • minilek 还询问这些已知的 (2-ε)^n 算法能否被某个宽泛而自然的算法类统一涵盖，讨论涉及细粒度复杂度（SETH 相关）框架。

为什么重要

  • ETH/SETH 是大量条件性下界（即「除非 ETH 失败，否则问题 X 没有快算法」）的基石。若其根基动摇，依赖它的 hardness 结果都需要重新审视。
  • 这场对话厘清了一个常见误解：下界并非对所有算法成立，而是针对归结等受限模型；现代 SAT 求解器恰好大体落在这类模型内，这使得下界对实践仍有解释力。PPSZ 等算法与下界条件的关系，正是判断「ETH 是否被现有技术威胁」的关键边界。

第 2 集 · 理论学家解析OpenAI破ETH求解器：属split and list算法(2026-10-30,2 条)

围绕 OpenAI 疑似违反指数时间假设(ETH)的 SAT 求解器,理论计算机科学家 Ryan Williams 分析指出,该算法属于「split and list」类方法:将变量拆分成块、块内暴力枚举,再借助 P 时间问题进行组合。Williams 表示他研究此类方法多年、曾试图打破 SETH,但令人惊讶的是,仅靠块内暴力枚举的策略就足以突破 ETH,且未来仍有改进空间。