AI 智能体穷举 SAT 证明 6 位 1 计数电路最少需 13 门

AI 智能体穷举 SAT 证明 6 位 1 计数电路最少 13 门

AI 导读

有智能体将 Knuth 遗留的一个小型开放问题拆成 3,735 个 SAT 子问题，在一台 8 核机器上跑了约 153 CPU 小时，得出不存在 12 门电路，答案应为恰好 13 门。作者表示尚未称其为已证明，独立评审仍在进行；抽样的 129 个 cube 中已有 123 个重新求解、全部为 UNSAT，其中 118 个已通过形式化验证的证明检查器。

正文 · AI 翻译

Larsen Cundric· @larsencc · X·2026-10-20 06:08· 20 分钟前AI 评分37

AI 导读

有智能体把 Knuth 遗留的一个小型开放问题拆成 3,735 个 SAT 子问题，在一台 8 核机器上跑了约 153 CPU 小时，得出不存在 12 门电路，答案应为恰好 13 门。

正文 · 原文

我让我的机器人去啃 Knuth 留下的一个小型开放问题

问题：判断 6 位中 1 的个数是否为 1 mod 3 的最小电路是什么？

已知答案至多为 13 门。此前没人把它确定到超过 5 个输入

我的机器人把它拆成 3,735 个 SAT 子问题，在一台 8 核机器上跑了约 153 CPU 小时

结果：不存在 12 门电路。所以答案应该是恰好 13 门

还不算已证明。独立审查仍在进行。抽样的 129 个立方体中已有 123 个重新求解，全部为 UNSAT，其中 118 个已由形式化验证的证明检查器检查过

附带发现：5 输入多数函数的最小 AND/OR 公式恰好是 14 个叶子。可能已知

不，这并没有解决 P vs NP 哈哈。这只是通往那里路上的微小精确案例 🫪

来源：Larsen Cundric · x.com

来源：RadarAI · aihot.news