A Moser-spindle-free 5-chromatic unit-distance graph on 766 vertices in the plane
收藏资源简介:
A unit-distance graph in the Euclidean plane with 766 vertices and 4074 edges, chromatic number exactly 5, containing no Moser spindle as a subgraph. The smallest previously published Moser-spindle-free 5-chromatic unit-distance graph has 1441 vertices. The graph also contains no regular unit hexagon. Coordinates are exact elements of Q(zeta_21): each point is (sum over k of a_k zeta_21^k)/7 with the integer coefficient vectors a given in graph766.json. Float coordinates are included for convenience only; all verification is exact. Files: graph766.json (exact and float coordinates, edge list, proper 5-colouring), verify.py (exact verifier: every listed edge has squared length exactly 1, no other pair does, no Moser spindle subgraph, included 5-colouring is proper), four_plain.cnf and four_symbreak.cnf (the 4-colouring formulas; both unsatisfiable, so the chromatic number is exactly 5), README.txt (usage and checksums). The DRAT unsatisfiability certificate of four_symbreak.cnf (472 MB, produced by kissat, checked with drat-trim: s VERIFIED; sha256 in README.txt) is attached as a release asset at https://github.com/chandanshukla1989/moser-free-766/releases/tag/v766 and can be regenerated with kissat. The graph was obtained by SAT-based vertex elimination (kissat with drat-trim proof-core extraction) from larger Moser-spindle-free constructions. Current development version: https://github.com/chandanshukla1989/moser-free-766



