Solving (Weighted) Partial MaxSAT by Dynamic Local Search for SAT
Authors: Zhendong Lei, Shaowei Cai
IJCAI 2018 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | Experiments on PMS and WPMS benchmarks from the Max SAT Evaluations (MSE) 2016 and 2017 show that SATLike significantly outperforms state of the art local search solvers. |
| Researcher Affiliation | Academia | State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences School of Computer and Control Engineering, University of Chinese Academy of Sciences |
| Pseudocode | Yes | Algorithm 1: SATLike |
| Open Source Code | No | The paper does not contain any explicit statement or link indicating that the source code for the described methodology (SATLike) is publicly available. |
| Open Datasets | Yes | We evaluate SATLike on all benchmarks of PMS and WPMS problems from the Max SAT Evaluations (MSE) 2016 and 2017. |
| Dataset Splits | No | The paper refers to using benchmarks from the Max SAT Evaluations but does not provide specific details on training, validation, or test dataset splits (e.g., percentages or sample counts). It mentions that solvers were run 'on each instance' from the MSEs, implying usage of the predefined benchmark instances without further splitting details. |
| Hardware Specification | Yes | Our experiments were conducted on a workstation using an Intel(R) Core(TM) i7-4710MQ CPU with 2.50GHz, 4MB L3 cache and 16 GB RAM, running Ubuntu 14.04 Linux operation system. |
| Software Dependencies | Yes | SATLike is implemented in C++ and compiled by g++ with -O3 option. (...) running Ubuntu 14.04 Linux operation system. |
| Experiment Setup | Yes | There are 4 parameters in the SATLike solver: t: the number of samplings, used in the BMS heuristic; sp: the smooth probability, used in Weighting-PMS; h inc: the increment for each falsified clause each time, used in Weighting-PMS; ζ: the limit on maximum value on soft clause weight, used in Weighting-PMS. The parameters are tuned according to our experience, and are listed as followed: For PMS Random and PMS Crafted benchmark: t=15,sp=0.01,h inc=2,ζ=1; For PMS Industrial and PMS 2017 benchmarks: t=42,sp=0.000003,h inc=1,ζ=400; For WPMS Random and WPMS Crafted benchmark: sp=0.01; For WPMS Industrial and WPMS 2017 benchmarks: sp=0.0001; For all WPMS benchmarks: t=15; h inc=300 and ζ=500 iff soft clause average weight > 10000, otherwise h inc=3 and ζ=1; |