Certificates for excluding degree-7 extensions of the (3,9;32,104) census in R(3,10)
收藏资源简介:
This archive provides machine-checkable certificates for the following exclusion: no (3,10;40)-graph G contains a vertex v of degree 7 whose induced remainder G − N[v] has exactly 104 edges. Equivalently, none of the 39 graphs in the (3,9;32,104) census can occur as the remainder of a degree-7 vertex in a (3,10;40)-graph. Contents: the complete census, up to isomorphism, of 39 (3,9;32,104)-graphs in graph6 format, agreeing with the census count reported by Goedgebeur and Radziszowski (2013); one CNF formula for each graph (39); one DRAT proof for each formula (39), produced by CaDiCaL 3.0.1; one drat-trim checker transcript for each proof (39); run records containing the census, solver, checker, and program fingerprints; the programs used to generate and check the computation (close_entry_v2.py and degree_interface.py); SHA-256 manifests and a README giving commands to verify the files and re-check every proof; and the completed audit log, assembled from retained Terminal output and documenting the audit re-checks. All 39 formulas are unsatisfiable. All 39 retained DRAT proofs were accepted by drat-trim during the production run and in the recorded audit re-checks. The re-checks used the same checker on the same machine and are not claimed as independent verification. Reference for the census: J. Goedgebeur and S. P. Radziszowski, “New Computational Upper Bounds for Ramsey Numbers R(3,k),” Electronic Journal of Combinatorics 20(1) (2013), P30. https://doi.org/10.37236/2824 This dataset supports a manuscript in preparation by John McCrea. The included source code is released under the MIT License.



