Notice: The reproducibility variables underlying each score are classified using an automated LLM-based pipeline, validated against a manually labeled dataset. LLM-based classification introduces uncertainty and potential bias; scores should be interpreted as estimates. Full accuracy metrics and methodology are described in Coakley et alK. L. Coakley, T. Snelleman, H. Hoos, and O. E. Gundersen, "The embrace of open science: An analysis of a decade of AI research and 56 800 conference papers," Under Review, 2026..
Schur Number Five
Authors: Marijn Heule
AAAI 2018 | Venue PDF | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | We obtained the solution, n = 160, by encoding the problem into propositional logic and applying massively parallel satisfiability solving techniques on the resulting formula. We constructed and validated a proof of the solution to increase trust in the correctness of the multi-CPU-year computations. |
| Researcher Affiliation | Academia | Marijn J. H. Heule Computer Science Department The University of Texas at Austin 2317 Speedway, M/S D9500 Austin, Texas 78712-0233 |
| Pseudocode | No | The paper describes methods and algorithms in text but does not include structured pseudocode or algorithm blocks. |
| Open Source Code | Yes | The tools and proof parts presented in this paper are available at https://www.cs.utexas.edu/~marijn/Schur/. |
| Open Datasets | No | The paper does not use a traditional dataset in the machine learning sense, but rather a mathematical problem encoding. No explicit public access information (link, DOI, formal citation) for a dataset is provided. |
| Dataset Splits | No | The paper solves a mathematical SAT problem and does not describe training, validation, or test dataset splits in the context of machine learning experiments. |
| Hardware Specification | Yes | We solved the subproblems on the Lonestar 5 cluster of the Texas Advanced Computing Center (TACC). Each compute node consists of a Xeon E5-2690 v3 (Haswell) chip with 24 cores running on 2.6 GHz. |
| Software Dependencies | Yes | For each cube α P 5, we solved2 the problem R5 160 α using our cube-and-conquer solver consisting of a modified version of MARCH CU (Heule et al. 2012) as look-ahead (cube) solver and GLUCOSE 3.0 (Audemard and Simon 2009) as CDCL (conquer) solver. |
| Experiment Setup | Yes | Examples of effective values are e = 1.0 and f = 0.6, e = 0.5 and f = 0.1, and e = 0.3 and f = 0.02. For the final experiments we used e = 0.3 and f = 0.02. |