A Modularity-Based Random SAT Instances Generator
Authors: Jesús Giráldez-Cru, Jordi Levy
IJCAI 2015 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | We evaluate the adequacy of this model to real industrial problems in terms of SAT solvers performance, and show that modern solvers do actually exploit this community structure. |
| Researcher Affiliation | Academia | Jes us Gir aldez-Cru and Jordi Levy IIIA CSIC Campus UAB, Bellaterra, Spain |
| Pseudocode | Yes | Algorithm 1: Community Attachment |
| Open Source Code | Yes | This modularity-based SAT generator is available in http://www.iiia.csic.es/ jgiraldez/software |
| Open Datasets | No | The paper generates its own random SAT instances for evaluation using the described model. It does not use a pre-existing publicly available dataset for training or evaluation. |
| Dataset Splits | No | The paper generates random instances based on specified parameters (n, m/n, Q, c) and then evaluates them. It does not describe standard training, validation, or test splits of a fixed dataset. |
| Hardware Specification | No | The paper mentions the use of SAT solvers (MiniSat, Glucose, March) but does not provide any specific details about the hardware (CPU, GPU, RAM) used for running the experiments. |
| Software Dependencies | No | The paper mentions specific SAT solvers used (Mini Sat, Glucose, March) and an algorithm from a prior work, but it does not specify version numbers for these software components, which is required for reproducibility. |
| Experiment Setup | Yes | We have generated some sets of random formulas for different values of Q {0.9, 0.8, 0.7, 0.5, 0.3} (hence P = Q + 1/c). ... The input number of communities c is fixed to 40. ... The timeout is set to 3 hours. |