Improving the Lower Bound in Branch-and-Bound Algorithms for MaxSAT
Authors: Shuolin Li, Chu-Min Li, Jordi Coll, Djamal Habet, Felip Manyà
AAAI 2025 | Venue PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | Experimental results show that this unlocking mechanism consistently improves the performance of a state-of-the-art Bn B solver. In addition, it allowed us to win the first two places in the exact unweighted category of the Max SAT Evaluation 2024. ... Experimental results on benchmarks from the Max SAT Evaluations 2019-2023 demonstrate that the unlocking mechanism consistently enhances the performance of both WMax CDCL and Max CDCL. |
| Researcher Affiliation | Academia | 1Aix Marseille Universit e, Universit e de Toulon, CNRS, LIS, Marseille, France 2Universit e de Picardie Jules Verne, Amiens, France 3Universitat de Girona, Girona, Spain 4Artificial Intelligence Research Institute, CSIC, Bellaterra, Spain |
| Pseudocode | Yes | Algorithm 1: Lookahead(H, S, α, UB), the algorithm to compute LB Algorithm 2: WLookahead(H, (S, w), α, UB), the algorithm to compute LB for weighted Max SAT |
| Open Source Code | Yes | The source code is available on the MSE24’s website under the name (W)Max CDCL. |
| Open Datasets | Yes | Experimental results on benchmarks from the Max SAT Evaluations 2019-2023 demonstrate that the unlocking mechanism consistently enhances the performance of both WMax CDCL and Max CDCL. |
| Dataset Splits | No | No specific training/test/validation splits are provided in the paper. The paper uses 'all instances of the weighted and unweighted exact tracks of the Max SAT evaluation (MSE) from 2019 to 2023' and categorizes them into subsets like '(W)MS19-20', '(W)MS19-(W)MS23' for analysis, but this does not constitute dataset splits for training or testing within an instance. |
| Hardware Specification | Yes | All experiments ran on Intel Xeon CPUs E5-2680@2.40GHz under Linux with 31GB of memory. |
| Software Dependencies | No | The paper mentions solvers like WMax CDCL, Max CDCL, and Open-WBO, but does not provide specific version numbers for these or any other ancillary software (e.g., programming languages, libraries, operating system versions) used in their experiments. |
| Experiment Setup | Yes | The timeout is set to 3600s per instance, as in MSE. ... Using Open WBO as a preprocessing during 1200s and 300s respectively, WMax CDCL and Max CDCL won the first two places of the exact unweighted category. |