遇见数据集

Independent Computational Verification of R(5,5) Extension Barriers: Exhaustive SAT Analysis of All 656 Known Ramsey(5,5) Graphs on 42 Vertices

收藏
Zenodo2026-05-29 更新2026-06-05 收录
官方服务:

资源简介:

We present an independent computational verification that none of the 656 tested instances obtained from McKay's catalog of Ramsey(5,5) graphs on 42 vertices admits a one-vertex extension to 43 vertices while preserving the Ramsey(5,5) property (i.e., remaining free of monochromatic K5 cliques and I5 independent sets). For each core G, the one-vertex extension problem is formulated as a propositional satisfiability (SAT) instance on 42 Boolean variables and solved using the CaDiCaL 1.5.3 solver via the PySAT interface. All 656 instances are rigorously proven unsatisfiable (UNSAT) in less than 2 minutes of total computational time. We also formulate and analyze an optimization version of the extension problem, introducing the pseudo-Boolean cost function Φ(x) which represents the count of monochromatic 5-subsets containing the new vertex in the extended 43-vertex graph. Empirically, the minimum value of Φ(x) is exactly 2 for every tested core, demonstrating a severe state of combinatorial frustration. Furthermore, an exhaustive one-edge-flip analysis in the full 43-vertex neighborhood shows that the cost cannot be reduced below 2 by any single flip. We observe and document a "Conflict Conservation Law" -- a local type-switching topological barrier where optimal flips destroy both I5 conflicts but are structurally forced to create exactly two K5 conflicts (or vice versa), trapping local heuristic search methods in infinite energy basin loops. Included Package Structure: - paper.md: Full academic report and mathematical formulation. - README.md: Reproduction and installation instructions. - code/prove_all_cores.py: Batch SAT proof runner script. - code/conservation_law.py: Highly optimized incremental 1-flip scanner script. - data/: McKay's original g6 catalog, SAT results, and 43-vertex minimum-cost witnesses. - logs/: Full execution logs and independent peer reviews from Claude 4.6 (Opus), Claude 4.7, and GPT-5.4. All computations and cognitive synthesis steps were driven by the ANTIGRAVITY AGI-DRIVE hybrid development node, co-authored by Paulina Janowska and Gniewisława (AI). Visit the cognitive portal for detailed trace records: https://gniewka.antydizajn.pl.

提供机构:
Zenodo
创建时间:
2026-05-29
二维码
社区交流群
二维码
科研交流群
商业服务