AI 中文总结
本文构造了112顶点的无桥三次图作为彼得森着色猜想的反例，经SAT求解器验证其无彼得森着色，结合相关定理可推出无穷多此类图无该着色。
AI 中文摘要
我们给出了一个顶点数为112的明确简单无桥三次图，该图没有彼得森着色，因此也没有正规5-边着色。该图在定理1.1中由SHA-256摘要标识，它由三个四极体L和一个爪六极体C组装而成；反过来，L由四个四极体F和一个C组装而成，其中F是通过删除彼得森图的一条边的端点得到的。我们为彼得森着色和正规5-边着色给出了直接的SAT公式，CaDiCaL 3.0.1对这两个公式均返回UNSAT，且drat-trim验证了所得的DRAT证明。辅助归档包含构造过程、明确的重新标记、编码器、证书、哈希值和验证程序。结合Ma、Mattiolo、Steffen和Wolf的定理，该反例还意味着存在无穷多个连通简单无桥三次图没有彼得森着色。我们还给出了一个单独验证的、非同构的D₃对称112顶点反例，我们未探讨112是否为最小值。
英文摘要
We give an explicit simple bridgeless cubic graph on 112 vertices with no Petersen coloring, and hence no normal 5-edge-coloring. The graph is identified by the SHA-256 digest in Theorem 1.1. It is assembled from three copies of a four-pole L and a claw six-pole C; in turn, L is assembled from four copies of a four-pole F and one copy of C, where F is obtained from the Petersen graph by deleting the endpoints of one edge. We give direct SAT formulations for Petersen colorings and normal 5-edge-colorings. CaDiCaL 3.0.1 returned UNSAT for both formulas, and drat-trim verified the resulting DRAT proofs. The ancillary archive contains the construction, an explicit relabeling, the encoders, certificates, hashes, and verification programs. Combined with a theorem of Ma, Mattiolo, Steffen, and Wolf, the counterexample also implies that infinitely many connected simple bridgeless cubic graphs have no Petersen coloring. We also give a separately verified, nonisomorphic $D_3$-symmetric 112-vertex counterexample. We do not address whether 112 is minimum.
Comments13 pages, 3 figures. Computer-assisted proof. Reproducibility artifacts and checked DRAT certificates are available at https://doi.org/10.5281/zenodo.21845291
