Artifacts for the r_3(212) computational campaign
收藏资源简介:
This dataset accompanies the manuscript "Salem-Spencer sets as across-solver benchmark: decomposition, certification, and split-policyeffects at r_3(212)" (arXiv:2606.04016). The release contains the citable computational artifacts for a cross-solverstudy of whether a 44-element subset of [1,212] can avoid every three-termarithmetic progression. No feasible 44-set was found. A verified43-element witness establishes r_3(212) >= 43, but the upper bound remainsopen, so the certified conclusion is r_3(212) in {43,44}. Artifacts include deterministic instance generators, benchmark JSONL andDIMACS instances, model-audit outputs, CP-SAT, HiGHS, CaDiCaL, and kissatresults, independently verified CNF/DRAT/LRAT certificate chains for the20 audited hard-pocket chunks, exact-value regression certificates forN = 80, 90, and 100 accepted by the formally verified cake_lpr checker,split-policy ablation results, an independently audited 96,847-cubeglobal-degree cover, and six solve-time-stratified certified survivorclosures. The released T2 portfolio closes 6,045 of 6,071 residual chunks withoutproof logging, leaving 26 UNKNOWN and no SAT result. These partial andsampled results do not constitute a proof of r_3(212) = 43 because nocomplete cube cover has been certificate-checked. Source snapshot:https://github.com/memoatwit/erdos_1194/tree/mpc-submission-v1.2/erdos_r3 Preprint:https://arxiv.org/abs/2606.04016



