Enhancing Local Search for MaxSAT with Deep Differentiation Clause Weighting
- URL: http://arxiv.org/abs/2512.05619v1
- Date: Fri, 05 Dec 2025 11:02:17 GMT
- Title: Enhancing Local Search for MaxSAT with Deep Differentiation Clause Weighting
- Authors: Menghua Jiang, Haokai Gao, Shuhao Chen, Yin Chen,
- Abstract summary: Partial Maximum Satisfiability (PMS) and weighted Partial Maximum Satisfiability (WPMS) generalize with broad real-world applications.<n>Existing methods often fail to adequately distinguish between PMS and WPMS.<n>We present a novel clause weighting scheme that updates the clause weights of PMS and WPMS according to distinct conditions.
- Score: 2.426267795975439
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Partial Maximum Satisfiability (PMS) and Weighted Partial Maximum Satisfiability (WPMS) generalize Maximum Satisfiability (MaxSAT), with broad real-world applications. Recent advances in Stochastic Local Search (SLS) algorithms for solving (W)PMS have mainly focused on designing clause weighting schemes. However, existing methods often fail to adequately distinguish between PMS and WPMS, typically employing uniform update strategies for clause weights and overlooking critical structural differences between the two problem types. In this work, we present a novel clause weighting scheme that, for the first time, updates the clause weights of PMS and WPMS instances according to distinct conditions. This scheme also introduces a new initialization method, which better accommodates the unique characteristics of both instance types. Furthermore, we propose a decimation method that prioritizes satisfying unit and hard clauses, effectively complementing our proposed clause weighting scheme. Building on these methods, we develop a new SLS solver for (W)PMS named DeepDist. Experimental results on benchmarks from the anytime tracks of recent MaxSAT Evaluations show that DeepDist outperforms state-of-the-art SLS solvers. Notably, a hybrid solver combining DeepDist with TT-Open-WBO-Inc surpasses the performance of the MaxSAT Evaluation 2024 winners, SPB-MaxSAT-c-Band and SPB-MaxSAT-c-FPS, highlighting the effectiveness of our approach. The code is available at https://github.com/jmhmaxsat/DeepDist
Related papers
- BanditSpec: Adaptive Speculative Decoding via Bandit Algorithms [101.9736063064503]
Speculative decoding has emerged as a popular method to accelerate the inference of Large Language Models (LLMs)<n>This paper proposes a training-free online learning framework to adaptively choose the configuration of the hyper parameters for speculative decoding as text is being generated.
arXiv Detail & Related papers (2025-05-21T05:56:31Z) - LLaMA-Berry: Pairwise Optimization for O1-like Olympiad-Level Mathematical Reasoning [56.273799410256075]
The framework combines Monte Carlo Tree Search (MCTS) with iterative Self-Refine to optimize the reasoning path.
The framework has been tested on general and advanced benchmarks, showing superior performance in terms of search efficiency and problem-solving capability.
arXiv Detail & Related papers (2024-10-03T18:12:29Z) - Rethinking the Soft Conflict Pseudo Boolean Constraint on MaxSAT Local
Search Solvers [20.866863965121013]
MaxSAT is an optimization version of the famous NP-complete Satisfiability problem (SAT)
We propose a new local search algorithm called SPB-MaxSAT that provides new perspectives for clause weighting on MaxSAT local search solvers.
arXiv Detail & Related papers (2024-01-19T09:59:02Z) - Combinatorial Stochastic-Greedy Bandit [79.1700188160944]
We propose a novelgreedy bandit (SGB) algorithm for multi-armed bandit problems when no extra information other than the joint reward of the selected set of $n$ arms at each time $tin [T]$ is observed.
SGB adopts an optimized-explore-then-commit approach and is specifically designed for scenarios with a large set of base arms.
arXiv Detail & Related papers (2023-12-13T11:08:25Z) - On Pitfalls of Test-Time Adaptation [82.8392232222119]
Test-Time Adaptation (TTA) has emerged as a promising approach for tackling the robustness challenge under distribution shifts.
We present TTAB, a test-time adaptation benchmark that encompasses ten state-of-the-art algorithms, a diverse array of distribution shifts, and two evaluation protocols.
arXiv Detail & Related papers (2023-06-06T09:35:29Z) - Towards Tackling MaxSAT by Combining Nested Monte Carlo with Local
Search [10.70006528984961]
We introduce two algorithmic variations over UCTMAXSAT.
First, a nesting of the tree search inspired by the Nested Monte Carlo Search algorithm is effective on most instance types in the benchmark.
Second, we observe that using a static flip limit in SLS, the ideal budget depends heavily on the instance size and we propose to set it dynamically.
arXiv Detail & Related papers (2023-02-26T03:37:26Z) - Incorporating Multi-armed Bandit with Local Search for MaxSAT [16.371916145216737]
Two generalizations of the MaxSAT problem: Partial MaxSAT (PMS) and Weighted PMS (WPMS)
We propose a local search algorithm for these problems, called BandHS, which applies two multi-armed bandits to guide the search directions when escaping local optima.
These two bandits can improve the algorithm's search ability in both feasible and infeasible solution spaces.
arXiv Detail & Related papers (2022-11-29T08:19:26Z) - DPMS: An ADD-Based Symbolic Approach for Generalized MaxSAT Solving [45.21499915442282]
We propose a novel dynamic-programming approach for solving generalized MaxSAT problems with hybrid constraints.
Our versatile framework admits many generalizations of CNF-MaxSAT, such as MaxSAT, Min-MaxSAT, and MinSAT with hybrid constraints.
Empirical results indicate that DPMS is able to solve certain problems quickly, where other algorithms based on various techniques all fail.
arXiv Detail & Related papers (2022-05-08T00:31:53Z) - Contrastive Proposal Extension with LSTM Network for Weakly Supervised
Object Detection [52.86681130880647]
Weakly supervised object detection (WSOD) has attracted more and more attention since it only uses image-level labels and can save huge annotation costs.
We propose a new method by comparing the initial proposals and the extension ones to optimize those initial proposals.
Experiments on PASCAL VOC 2007, VOC 2012 and MS-COCO datasets show that our method has achieved the state-of-the-art results.
arXiv Detail & Related papers (2021-10-14T16:31:57Z) - Farsighted Probabilistic Sampling based Local Search for (Weighted)
Partial MaxSAT [5.529868797285073]
Partial MaxSAT (PMS) and Weighted Partial MaxSAT (WPMS) are practical generalizations to the typical problem of MaxSAT.
We propose an effective farsighted probabilistic sampling based local search algorithm called FPS for solving these two problems.
arXiv Detail & Related papers (2021-08-23T07:41:56Z)
This list is automatically generated from the titles and abstracts of the papers in this site.
This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.