AI 机器人用 SAT 求解证明 6 位 1 mod 3 电路需 13 门
I let my bots grind on a tiny open case Knuth left behind
作者让机器人把 Knuth 遗留的一个小开放问题拆成 3,735 个 SAT 子问题，在单台 8 核机器上跑了约 153 CPU 小时，得出不存在 12 门电路，答案应为 13 门。此前已知上界为 13 门，但 5 个输入以上一直未确定。作者称尚未算证明，独立评审仍在进行：129 个抽样立方中 123 个已重新求解且全部 UNSAT，118 个已通过形式化验证的证明检查器。另发现 5 输入多数函数的最小 AND/OR 公式恰为 14 个叶子。
正文
当前显示原文，中文全文译文尚未就绪。
I let my bots grind on a tiny open case Knuth left behind
Question: whats the smallest circuit that tells you if the number of 1s in 6 bits is 1 mod 3?
Known answer was at most 13 gates. Nobody had pinned it down past 5 inputs
My bots split it into 3,735 SAT sub-problems and ran ~153 CPU hours on one 8 core box
Result: no 12 gate circuit exists. So the answer should be exactly 13
Not calling it proven yet. Independent review is still running. 123 of 129 sampled cubes re-solved, all UNSAT, and 118 already checked by a formally verified proof checker
Side find: smallest AND/OR formula for 5 input majority is exactly 14 leaves. Might already be known
No this doesn't solve P vs NP lol. This is just tiny exact cases on the way there