遇见数据集

Certified SAT artifacts for Frankl's union-closed sets conjecture under transitive group symmetry on 14 points (DRAT certificates for the five minimal instances)

收藏
Zenodo2026-08-13 更新2026-08-20 收录
官方服务:

资源简介:

Heavy computational artifacts supporting the repository frankl-transitive-sat: a computer-assisted proof that no non-trivial union-closed family on 14 points invariant under any transitive permutation group violates Frankl's union-closed sets conjecture. Via an invariance-descent lemma and a reduction to minimal transitive groups (census: 63 transitive groups of degree 14, of which 26 contain no 14-cycle), the theorem reduces to the already-certified cyclic case Z14 (doi:10.5281/zenodo.21900943) plus five group instances: 14T2 (regular D7), 14T6 ([2^3]7), 14T10 (L7(14)), 14T12 (1/2[D(7)^2]2) and 14T30 (PSL(2,13) on the projective line). Each of the five is UNSAT for family size ≥ 3 (sizes ≤ 2 conform trivially, Sarvate–Renaud reduction), decided by two independent exact methods — OR-Tools CP-SAT and CaDiCaL on an independently written encoding — and every CaDiCaL refutation carries the DRAT certificate archived here, verified with drat-trim (s VERIFIED on all five). Files (xz-compressed; SHA-256 of the compressed files in SHA256SUMS-certificates.txt): for each group G in {14T2, 14T6, 14T10, 14T12, 14T30} — G.cnf.xz, the DIMACS instance (deterministic output of the repository's dump_dimacs_group.py G 3), and G.drat.xz, its verified DRAT unsatisfiability certificate (14T2.drat is 3.3 GB decompressed). Verification recipe: unxz both files of a group, check the hashes, then run drat-trim G.cnf G.drat; expected output s VERIFIED. 14T30, 14T12 and 14T10 verify in under a second, 14T6 in about 4 seconds, 14T2 in about 50 minutes with <2 GB RAM. Full mathematical statements, the group census and minimality scan, measured resource data and reproduction instructions: see the repository's README.md, docs/theorem-degree14.md and results/FOUND.md. The computations were executed autonomously by an AI agent loop built on Anthropic's Claude Code under human supervision.

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