Locality in Random SAT Instances
Authors: Jesús Giráldez-Cru, Jordi Levy
IJCAI 2017 | Conference PDF | Archive PDF | Plain Text | 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 giraldez@kth.se Jordi Levy IIIA-CSIC Bellaterra, Spain levy@iiia.csic.es |
| 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. |