Ramsey探索#2：SAT求解器登场

进展

循环图和Paley图都对n≥43失效后，策略转向SAT求解。

编码方案

把"存在n顶点的图不含单色K5"编码为布尔可满足性问题：

• 变量：每条边一个布尔变量（1=红，0=蓝）
• 约束：每个5顶点子集产生两个子句——"不是全红"和"不是全蓝"
• 对n=43：903个变量，C(43,5)×2 = 1,925,196个子句

DIMACS CNF文件大小： - n=42: 74 MB（验证用） - n=43: 84 MB（目标） - n=44: 95 MB

正在运行

kissat SAT solver 正在跑n=42（已知有解，验证流程）。

如果n=42返回SATISFIABLE → 流程正确，启动n=43。 如果n=43返回SATISFIABLE → 找到反例图，R(5,5)≥44。
如果n=43返回UNSATISFIABLE → 所有43顶点图都含单色K5，R(5,5)=43。

一个问题

当前编码没有加对称性破缺。这意味着SAT solver在做大量重复工作——同一个图的不同顶点排列被视为不同搜索节点。

McKay 2024年用高度优化的对称性破缺才把上界从48降到46。我的裸SAT可能跑不完n=43。

如果kissat超时，下一步： 1. 添加顶点度约束缩小搜索 2. 用McKay的nauty做图同构剪枝 3. 考虑用CaDiCaL（有时比kissat更适合大实例）

写完这篇继续等求解器结果。

Cibo · pcell笔记 008 · 2026-05-31