From Decimation to Local Search and Back: A New Approach to MaxSAT
Authors: Shaowei Cai, Chuan Luo, Haochen Zhang
IJCAI 2017 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | Experiments show that our solver Deci LS achieves state of the art performance on all unweighted benchmarks from the Max SAT Evaluation 2016. |
| Researcher Affiliation | Academia | 1State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, China 2School of Computer and Control Engineering, University of Chinese Academy of Sciences, China 3Institute of Computing Technology, Chinese Academy of Sciences, China |
| Pseudocode | Yes | Algorithm 1: A UP-based Decimation Algorithm for Max SAT |
| Open Source Code | No | The paper states that the source code for CCAnr, a third-party local search solver they modified, is available online. However, it does not provide a link or explicit statement about the availability of their own implementation of Deci LS, Deci Dist, or Deci CCEHC, which represent their core contribution. |
| Open Datasets | Yes | We evaluate Deci LS on all random, crafted and industrial benchmarks of unweighted Max SAT from the MSE2016. Also, we conduct experiments on Application instances from the SAT Competition (SC) 2016 |
| Dataset Splits | No | The paper mentions using established benchmarks from MSE2016 and SAT Competition 2016 but does not specify the train/validation/test splits used for their experiments, nor does it cite a reference for a standard splitting methodology that could be reproduced. |
| Hardware Specification | Yes | All experiments in this work are carried out on a cluster of workstations equipped with Intel Xeon E7-8830 2.13 GHz CPU, 24MB L3 cache and 1.0TB RAM under the operating system Cent OS (version: 7.0.1406). |
| Software Dependencies | No | The paper states that "Deci LS is implemented in C++ and compiled by g++ with -O3 option." This mentions the language and compiler but does not provide specific version numbers for any libraries, frameworks, or other software dependencies beyond the operating system version. |
| Experiment Setup | Yes | There are two parameters in Deci LS: parameter k for the BMS heuristic used in the decimation algorithm and Max Non Improve for local search. We tune these parameters with the automatic configuration tool SMAC [Hutter et al., 2011], and set k = 20 and Max Non Improve = 50000 for all benchmarks. ... Max Non Improve is set to 10000000 for local search in Deci Dist. |