BandMaxSAT: A Local Search MaxSAT Solver with Multi-armed Bandit
Authors: Jiongzhi Zheng, Kun He, Jianrong Zhou, Yan Jin, Chu-Min Li, Felip Manyà
IJCAI 2022 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | Extensive experiments demonstrate that Band Max SAT significantly outperforms the stateof-the-art (W)PMS local search algorithm SATLike3.0. Specifically, the number of instances in which Band Max SAT obtains better results is about twice that obtained by SATLike3.0. Moreover, we combine Band Max SAT with the complete solver TT-Open-WBO-Inc. The resulting solver Band Max SAT-c also outperforms some of the best state-of-the-art complete (W)PMS solvers, including SATLike-c, Loandra and TT-Open-WBO-Inc. |
| Researcher Affiliation | Academia | Jiongzhi Zheng1,2 , Kun He 1 , Jianrong Zhou1 , Yan Jin1 , Chu-Min Li3 , Felip Manya4 1School of Computer Science and Technology, Huazhong University of Science and Technology 2Institute of Artificial Intelligence, Huazhong University of Science and Technology, China 3MIS, University of Picardie Jules Verne, France 4Artificial Intelligence Research Institute (IIIA), CSIC, Bellaterra, Spain |
| Pseudocode | Yes | Algorithm 1: Hy Deci(F) ... Algorithm 2: Pick Arm(Arm Num, N, λ) ... Algorithm 3: Band Max SAT |
| Open Source Code | Yes | The code of Band Max SAT is available at https://github.com/JHLHUST/Band Max SAT/. |
| Open Datasets | Yes | We tested the algorithms on all the (W)PMS instances from the incomplete track of last four Max SAT Evaluations (MSE), i.e., MSE2018-MSE2021. ... We use all the (W)PMS instances from the incomplete track of MSE2017 as the training set to tune these parameters. |
| Dataset Splits | Yes | We use all the (W)PMS instances from the incomplete track of MSE2017 as the training set to tune these parameters. |
| Hardware Specification | Yes | Our experiments were performed on a server using an Intel Xeon E5-2650 v3 2.30 GHz 10-core CPU and 256 GB RAM, running Ubuntu 16.04 Linux operation system. |
| Software Dependencies | No | Band Max SAT is implemented in C++ and compiled by g++. No specific version numbers for g++ or any other software dependencies are provided. |
| Experiment Setup | Yes | The parameters in Band Max SAT include the BMS parameter k, the reward delay steps d, the reward discount factor γ, the number of sampled arms Arm Num, and the exploration bias parameter λ. ... Finally, the default settings of these parameters are as follows: k = 15, d = 20, γ = 0.9, Arm Num = 20, λ = 1. |