Satisfiability and Algorithms for Non-uniform Random k-SAT
Authors: Oleksii Omelchenko, Andrei Bulatov3886-3894
AAAI 2021 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | In this section we report the results of some computational experiments we conducted with Configuration Model, in which ξ is the zeta distribution. The experiments pursued the following goals: (a) to estimate the actual location of the satisfiability/unsatisfiability borderline; (b) to evaluate the success rate of Algorithm 2 for different values of the parameter α. Experiments were performed on machines with 32Gb of RAM and Intel Core i7-6700 CPU, and we had 6 threads working in parallel generating instances and solving them on each computer. |
| Researcher Affiliation | Academia | Oleksii Omelchenko, Andrei A. Bulatov Simon Fraser University, Burnaby BC, Canada oomelche@sfu.ca, abulatov@sfu.ca |
| Pseudocode | Yes | Algorithm 1 Configuration Model Ck n(ξ) and Algorithm 2 ISSAT(φ) |
| Open Source Code | No | The paper does not provide explicit statements about the release of their own source code for the described methodology (e.g., a specific repository link, an explicit code release statement, or code in supplementary materials). |
| Open Datasets | No | We generated two collections of 3-SAT formulas, one with n = 106 variables and another one with n = 2 106 variables. This refers to internally generated data, not a publicly available dataset with concrete access information (link, DOI, citation). |
| Dataset Splits | No | The paper describes generating instances of SAT formulas and solving them, but does not specify dataset splits (e.g., train/validation/test percentages or counts) in a way that applies to typical machine learning model reproduction. The evaluation is done on generated SAT instances. |
| Hardware Specification | Yes | Experiments were performed on machines with 32Gb of RAM and Intel Core i7-6700 CPU, and we had 6 threads working in parallel generating instances and solving them on each computer. |
| Software Dependencies | Yes | We generated two collections of 3-SAT formulas, one with n = 106 variables and another one with n = 2 106 variables. For each n {106, 2 106} and every β {2.30, 2.35, 2.40, . . . , 2.95, 3.00} we created 2048 formulas from C3 n(ξ), which we solved using Crypto Mini SAT 5.6.6 with default parameters, and calculated the fraction of satisfiable formulas among those instances (see Figure 1a). |
| Experiment Setup | Yes | For each n {106, 2 106} and every β {2.30, 2.35, 2.40, . . . , 2.95, 3.00} we created 2048 formulas from C3 n(ξ), which we solved using Crypto Mini SAT 5.6.6 with default parameters, and calculated the fraction of satisfiable formulas among those instances (see Figure 1a). The experiment s set up was the following. We created 10,000 instances for each model, for each average variable s degree from the set {1.1, 1.2, 1.3, . . . , 13.2, 13.3, 13.4}, and for the number of variables n {100, 200, 300}... |