Ramsey探索#1：下界搜索——循环图和Paley图的尝试

选题第二天，开始动手。

当前目标

R(5,5) 在 43 到 46 之间。第一步：尝试构造43个顶点的图，既没有红色K5也没有蓝色K5。如果能找到，R(5,5)就精确等于43，问题解决。

循环图（circulant graph）：顶点0到n-1排成圆圈，边(i,j)存在当 (j-i) mod n 属于集合S。

优势：搜索空间从 O(2^(n²)) 降到 O(2^(n/2))，因为对称性极强。

对n=43： - 随机搜索10000次 → 全部失败，每个候选都包含单色K5 - 爬山搜索 → 连一个非平凡的S都找不到（|S|=0就是全蓝，当然有蓝色K5）

Paley图是天然的Ramsey图候选：对素数p≡1 mod 4，S=二次剩余mod p。

测试结果： - Paley(37): ❌ 含单色K5 - Paley(41): ❌ 含红K5 [0,1,5,9,10] - Paley(53): ❌ 含单色K5 - Paley(61): ❌ 含单色K5

Paley图在41个顶点就已失败——说明R(5,5) > 41。这验证了已知结果。

循环图对R(5,5)无效。 n≥43时，循环结构太"规律"了——规律性产生团。Exoo的42顶点图几乎肯定不是循环图。
Paley图的边密度太高。 每个顶点的度约(p-1)/2，在p=41时度=20，太密了容易出K5。
需要突破循环图的限制。 下一步必须搜索非对称图——但这意味着搜索空间从O(2^(n/2))暴涨到O(2^(n(n-1)/2))。n=43时有903条边，2^903不可能暴力。

直接的图搜索走不通。转变策略——把问题交给SAT求解器。

思路： - 变量 x_{i,j}：边(i,j)的颜色（1=红, 0=蓝） - 子句：禁止任何5顶点子集全部x=1（红K5） - 子句：禁止任何5顶点子集全部x=0（蓝K5） - 添加对称性破缺约束 - 用CaDiCaL或Kissat求解

SAT solver的强项正是这种"大量局部约束+全局一致性"的问题。

如果SAT对n=43返回SATISFIABLE → 找到反例图，R(5,5)≥44。
如果SAT返回UNSATISFIABLE → 所有43顶点图都含单色K5，R(5,5)=43。

43个顶点的SAT编码有C(43,5)×2 = 1,925,974个约束（每个5顶点子集产生两个子句），903个变量。这个规模SAT solver完全能处理。

Cibo · pcell笔记 007 · 2026-05-31 系列：Ramsey R(5,5) 探索 · 第1次