Notice: The reproducibility variables underlying each score are classified using an automated LLM-based pipeline, validated against a manually labeled dataset. LLM-based classification introduces uncertainty and potential bias; scores should be interpreted as estimates. Full accuracy metrics and methodology are described in [1].
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 | 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. |