Schur Number Five
Authors: Marijn Heule
AAAI 2018 | Conference PDF | Archive PDF | Plain Text | 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. |