Rethinking the Soft Conflict Pseudo Boolean Constraint on MaxSAT Local Search Solvers
Authors: Jiongzhi Zheng, Zhuo Chen, Chu-Min Li, Kun He
IJCAI 2024 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | Extensive experiments demonstrate the excellent performance of the proposed methods. |
| Researcher Affiliation | Academia | 1School of Computer Science and Technology, Huazhong University of Science and Technology, China 2MIS, University of Picardie Jules Verne, France |
| Pseudocode | Yes | Algorithm 1: SPB-Max SAT |
| Open Source Code | Yes | 1https://github.com/JHL-HUST/SPB-Max SAT |
| Open Datasets | Yes | We evaluated the algorithms on all the PMS and WPMS instances from the incomplete track of the six recent MSEs2, i.e., MSE2018 to MSE2023. 2https://maxsat-evaluations.github.io/ |
| Dataset Splits | No | The paper states that algorithms were evaluated 'on all the PMS and WPMS instances from the incomplete track of the six recent MSEs', and parameters were tuned 'based on instances in the incomplete track of MSE2017'. While this implies usage of standard benchmark sets, the paper does not explicitly detail the train/validation/test dataset splits (e.g., percentages or sample counts) used for the experiments. |
| Hardware Specification | Yes | All the algorithms were implemented in C++ and run on a server using an AMD EPYC 7H12 CPU, running Ubuntu 18.04 Linux operation system. |
| Software Dependencies | No | The paper mentions implementation in C++ and running on Ubuntu 18.04, and the use of SMAC3 for parameter tuning, but does not provide specific version numbers for compilers, libraries, or other software dependencies beyond the operating system version. |
| Experiment Setup | Yes | Parameters in SPB-Max SAT mainly include the BMS parameter k, the hard clause dynamic weight increment hinc, and the increase proportion δ. The final settings of these parameters in both SPB-Max SAT and SPB-Max SAT-c are k = 53, hinc = 1, and δ = 1.00072 for PMS and k = 97, hinc = 28, and δ = 1.001 for WPMS. |