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..
Locality in Random SAT Instances
Authors: Jesús Giráldez-Cru, Jordi Levy
IJCAI 2017 | Venue PDF | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | In a first experiment, we show how VSIDS exploits both the popularity and the similarity of variables by analyzing the variables selected by the branching heuristic of the well-known CDCL SAT solver Minisat. |
| Researcher Affiliation | Academia | Jes us Gir aldez-Cru KTH Royal Institute of Technology Stockholm, Sweden EMAIL Jordi Levy IIIA-CSIC Bellaterra, Spain EMAIL |
| Pseudocode | No | The paper does not contain structured pseudocode or algorithm blocks clearly labeled as such. |
| Open Source Code | No | The paper does not provide concrete access to source code (specific repository link, explicit code release statement, or code in supplementary materials) for the methodology described in this paper. |
| Open Datasets | No | The paper describes generating random SAT instances based on a new model rather than using a publicly available or open dataset. No specific access information (link, DOI, repository, or formal citation with author/year) is provided for a dataset. |
| Dataset Splits | No | The paper describes generating random SAT instances with specific parameters for evaluation, rather than providing training/validation/test dataset splits of a pre-existing dataset. |
| Hardware Specification | No | The paper does not provide specific hardware details (exact GPU/CPU models, processor types with speeds, memory amounts, or detailed computer specifications) used for running its experiments. |
| Software Dependencies | No | The paper mentions software like Minisat, Glucose, and March, but does not provide specific version numbers for these or any other ancillary software components. |
| Experiment Setup | Yes | The size of the formulas is n = 5000 when T < 2, and n = 300 otherwise. Since we are just interested in analyzing the effects of popularity and similarity of variables in SAT solving performance and not the effects of different clause sizes , we limit our experimentation to the case β = 0, K = 3 and k = 0, i.e., all clauses of size 3. We always use m/n = 4.25. |