Unsatisfiability Proofs for Weight 16 Codewords in Lam's Problem
Authors: Curtis Bright, Kevin K.H. Cheung, Brett Stevens, Ilias Kotsireas, Vijay Ganesh
IJCAI 2020 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | Our searches completed in about 30 hours on a desktop machine and produced nonexistence proofs of about 1 terabyte in the DRAT (deletion resolution asymmetric tautology) format. |
| Researcher Affiliation | Academia | 1University of Waterloo, Department of Electrical and Computer Engineering 2Carleton University, School of Mathematics and Statistics 3Wilfrid Laurier University, Department of Physics and Computer Science |
| Pseudocode | No | The paper describes methods in text and uses mathematical notation but does not contain any structured pseudocode or clearly labeled algorithm blocks. |
| Open Source Code | Yes | The scripts used to generate and solve the SAT instances are available at uwaterloo.ca/mathcheck |
| Open Datasets | No | The paper refers to 'ten starting matrices' and mentions 'Full starting matrices for each case are available at uwaterloo.ca/mathcheck/w16.' However, these are problem instances/configurations, not a 'dataset' in the conventional sense that would be split for training, and no formal citation for a public dataset is provided. |
| Dataset Splits | No | The paper focuses on SAT solving to prove non-existence, not on a machine learning task requiring train/validation/test splits. No specific dataset split information is provided. |
| Hardware Specification | Yes | The computations were run on a desktop machine with an Intel i7 CPU at 2.7 GHz. |
| Software Dependencies | Yes | The computer algebra system Maple 2019 which uses the library nauty [Mc Kay and Piperno, 2014]. |
| Experiment Setup | Yes | The amount of cubing was controlled by the cubing cutoff -n parameter of March_cu (replacing the default heuristic cutoff). Typically starting with a cubing cutoff bound equal to about 75% of the free variables in the instance worked well and we tuned the bound higher or lower based on the solver performance. |