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

1. 06:08
   RadarAI

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

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

趋势仅比较持续完整观测到的相同主体，范围可能小于当前热度统计。移动指针或点击图表查看每小时热度；键盘可用左右方向键切换。