Double Configuration Checking in Stochastic Local Search for Satisfiability
Authors: Chuan Luo, Shaowei Cai, Wei Wu, Kaile Su
AAAI 2014 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | The experiments show that the DCCASat solver significantly outperforms a number of state-of-the-art solvers on extensive random k-SAT benchmarks at the phase transition. Moreover, DCCASat shows good performance on structured benchmarks, and a combination of DCCASat with a complete solver achieves state-of-the-art performance on structured benchmarks. |
| Researcher Affiliation | Academia | 1Key Laboratory of High Confidence Software Technologies of Ministry of Education, Peking University, Beijing, China 2State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing, China 3Queensland Research Laboratory, NICTA, Brisbane, Australia 4Institute for Integrated and Intelligent Systems, Griffith University, Brisbane, Australia |
| Pseudocode | Yes | Algorithm 1: The DCCA Heuristic; Algorithm 2: The pick Var Function of DCCASat |
| Open Source Code | No | The DCCASat solver is developed on the top of CCASat, and thus is implemented in C++. However, no explicit statement or link is provided for the open-sourcing of DCCASat's code. |
| Open Datasets | Yes | SC13_Threshold: all 250 random k-SAT instances from the threshold benchmark of the random SAT track of SAT Competition 20132 ... 2http://satcompetition.org/2013/files/sc13-benchmarksrandom.tgz; Large_Threshold: random k-SAT instances generated randomly at the threshold ratio of phase transition according to the random k-SAT generator3 used in SAT Competition 2013 ... 3http://sourceforge.net/projects/ksatgenerator/; SC13_HC: all 150 satisfiable instances from the hardcombinatorial SAT track of SAT Competition 20136 ... 6http://satcompetition.org/2013/files/sc13-benchmarkscombinatorial.tgz; The CBMC and SWV benchmarks7 are real world verification problems. ... 7https://cs.uwaterloo.ca/~dtompkin/papers/sat10-dave-instances.zip |
| Dataset Splits | No | The paper uses established benchmarks for evaluation but does not specify custom training, validation, or test splits, or cross-validation methodology for its experiments. |
| Hardware Specification | Yes | All experiments are carried out on a machine under GNU/Linux, using 2 cores of Intel Core i7 2.4GHz. |
| Software Dependencies | No | The DCCASat solver is implemented in C++. No specific version numbers for C++ or any other software libraries are provided. |
| Experiment Setup | Yes | For random 3-SAT, wt for SWT is set to 200 + n+250/500 , where n is the number of variables in the instance; p for SWT and q for SWT are set to 0.3 and 0.7, respectively. For random k-SAT with k > 3, d for hscore is set to 13k; β for hscore and γ for hscore2 are both set to 1000; sp for PAWS is set to 0.75 for 4-SAT, 0.8 for 5-SAT, 0.9 for 6-SAT and 0.92 for k-SAT with k 7. For structured instances, DCCASat performs a simple unit propagation procedure before the search; wt for SWT is set to 300; p for SWT is set to 0.3; q for SWT is set to 0 if α 15 and to 0.7 otherwise... |