遇见数据集

C(12,6,4) = 41 - unsatisfiability certificates

收藏
Zenodo2026-07-26 更新2026-08-01 收录
官方服务:

资源简介:

The 81 retained DRAT unsatisfiability certificates underlying the lower-boundcase analysis in "The covering number C(12,6,4) is 41": 47 case-tree frontierrefutations (46 against the sequential cardinality encoding, one — s-r0-2 —against the totalizer encoding), 14 auxiliary/exhaustiveness refutations, and20 link-extension refutations. All proofs are gzipped DRAT; every one wasreplayed with drat-trim and machine-checked via LRAT with cake_lpr, theCakeML/HOL4-verified checker. The archive contains a README, an index.json(per-proof compressed SHA-256 and raw byte length), and a MANIFEST.sha256. The paper's certificate inventory totals 83; the two beyond the 81 here aresecond-encoding duplicates of case instances already covered, recorded in theartifact by SHA-256 and byte length rather than deposited. Together theseproofs establish C(12,6,4) = 41, equivalently the Turán number T(12,8,6) = 41,from which four improved covering-number lower bounds follow. The CNF instances these proofs refute are not included here — they regeneratebyte-for-byte from the companion computational artifact, DOI10.5281/zenodo.21572070, whose manifests record each proof's hashes andverification verdicts. Also not deposited: the LRAT files, which regeneratedeterministically from these proofs via "drat-trim <cnf> <drat> -L", and thesecond-encoding DRAT sweep for 46 of the 47 frontier nodes; both are recordedby SHA-256 and byte length in the artifact's manifests and are available fromthe author on request. To unpack: mkdir c1264-certificates && tar -xf c1264-certificates-v1.0.0.tar -C c1264-certificatesThen: cd c1264-certificates && shasum -a 256 -c MANIFEST.sha256

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