An Efficient Core-Guided Solver for Weighted Partial MaxSAT
Authors: Shiwei Pan, Yiyuan Wang, Shaowei Cai
IJCAI 2025 | Venue PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | Experimental results on benchmarks from the complete weighted track of the Max SAT Evaluations 2022-2024 demonstrate that the proposed methods lead to substantial improvements, with CASHWMax SAT outperforming state-of-the-art Max SAT solvers across all benchmarks. Additionally, it enabled us to achieve the top two positions in the exact weighted category of the Max SAT Evaluation 2024. Extensive experiments are conducted to evaluate CASHWMax SAT on the complete weighted benchmarks of the Max SAT Evaluations from 2022 to 2024. |
| Researcher Affiliation | Academia | 1School of Computer Science and Information Technology, Northeast Normal University, China 2Key Laboratory of System Software, Institute of Software, Chinese Academy of Sciences 3Key Laboratory of Applied Statistics of MOE, Northeast Normal University, China 4School of Computer Science and Technology, University of Chinese Academy of Sciences, China EMAIL, EMAIL |
| Pseudocode | Yes | Algorithm 1: Stratification. Algorithm 2: MUS. Algorithm 3: MUCE. Algorithm 4: CASHWMax SAT. |
| Open Source Code | No | The paper states CASHWMax SAT was submitted to the Max SAT Evaluation 2024 and mentions it was developed based on COMini Sat PS SAT solver. While submission to an evaluation might imply some level of availability, there is no explicit statement by the authors about releasing their code (CASHWMax SAT) for public access or a direct link to its repository within the paper. Footnote 1 links to the general Max SAT Evaluation page, not specific source code for this paper's methodology. |
| Open Datasets | Yes | We selected all test instances from the complete weighted track of the Max SAT Evaluation (MSE) 2022, 2023, and 20242, resulting in a total of 1,736 instances. Footnote 2: https://maxsat-evaluations.github.io/ |
| Dataset Splits | No | The paper states that 'all test instances from the complete weighted track of the Max SAT Evaluation (MSE) 2022, 2023, and 2024' were used. For Max SAT solver evaluations, these are pre-defined benchmark instances to be solved, rather than a single dataset that is split into training/validation/test sets by the authors of this paper. Therefore, explicit training/test/validation splits are not applicable or provided within the paper's text for its own methodology. |
| Hardware Specification | Yes | All experiments were conducted on a system running Ubuntu 22.04.5 LTS, equipped with an Intel(R) Xeon(R) Platinum 8260 CPU @ 2.40GHz and 512GB of memory. |
| Software Dependencies | No | The paper mentions that CASHWMax SAT was 'Developed based on the COMini Sat PS SAT solver [Oh, 2016]' but does not provide a specific version number for COMini Sat PS. It also mentions 'implemented in C++11', which is a language standard, not a specific software tool with a version. While SCIP (version 8.1.0) is mentioned, it is in the context of competitor solvers and hybrid approaches, not as a core software dependency for CASHWMax SAT itself in its independent form, for which version details are requested. |
| Experiment Setup | Yes | For each test instance and algorithm, the runtime was set to 3,600 seconds, aligning with the competition s time limit. ... In our work, the termination condition of the SAT solver is that when the number of conflicts generated during the search reaches a certain threshold, the solver returns UNKNOWN. |