Rethinking the Soft Conflict Pseudo Boolean Constraint on MaxSAT Local Search Solvers

• URL: http://arxiv.org/abs/2401.10589v1
• Date: Fri, 19 Jan 2024 09:59:02 GMT
• Title: Rethinking the Soft Conflict Pseudo Boolean Constraint on MaxSAT Local Search Solvers
• Authors: Jiongzhi Zheng and Zhuo Chen and Chu-Min Li and Kun He
• Abstract summary: 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.
• Score: 20.866863965121013
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: MaxSAT is an optimization version of the famous NP-complete Satisfiability problem (SAT). Algorithms for MaxSAT mainly include complete solvers and local search incomplete solvers. In many complete solvers, once a better solution is found, a Soft conflict Pseudo Boolean (SPB) constraint will be generated to enforce the algorithm to find better solutions. In many local search algorithms, clause weighting is a key technique for effectively guiding the search directions. In this paper, we propose to transfer the SPB constraint into the clause weighting system of the local search method, leading the algorithm to better solutions. We further propose an adaptive clause weighting strategy that breaks the tradition of using constant values to adjust clause weights. Based on the above methods, we propose a new local search algorithm called SPB-MaxSAT that provides new perspectives for clause weighting on MaxSAT local search solvers. Extensive experiments demonstrate the excellent performance of the proposed methods.

Related papers

• Training Greedy Policy for Proposal Batch Selection in Expensive Multi-Objective Combinatorial Optimization [52.80408805368928]
  We introduce a novel greedy-style subset selection algorithm for batch acquisition. Our experiments on the red fluorescent proteins show that our proposed method achieves the baseline performance in 1.69x fewer queries.
  arXiv  Detail & Related papers  (2024-06-21T05:57:08Z)
• UpMax: User partitioning for MaxSAT [2.2022484178680872]
  partitioning has a large impact on the performance of unsatisfiability-based MaxSAT algorithms. This paper proposes a new framework called UpMax that decouples the partitioning procedure from the MaxSAT solving algorithms.
  arXiv  Detail & Related papers  (2023-05-25T15:50:00Z)
• DeciLS-PBO: an Effective Local Search Method for Pseudo-Boolean Optimization [10.513103815142731]
  We find two ways to improve the local search algorithms in solving Pseudo-Boolean Optimization (PBO) Our algorithm DeciLS-PBO has a promising performance compared to the state-of-the-art algorithms.
  arXiv  Detail & Related papers  (2023-01-28T17:03:56Z)
• 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)
• A Metaheuristic Algorithm for Large Maximum Weight Independent Set Problems [58.348679046591265]
  Given a node-weighted graph, find a set of independent (mutually nonadjacent) nodes whose node-weight sum is maximum. Some of the graphs airsing in this application are large, having hundreds of thousands of nodes and hundreds of millions of edges. We develop a new local search algorithm, which is a metaheuristic in the greedy randomized adaptive search framework.
  arXiv  Detail & Related papers  (2022-03-28T21:34:16Z)
• Learning Proximal Operators to Discover Multiple Optima [66.98045013486794]
  We present an end-to-end method to learn the proximal operator across non-family problems. We show that for weakly-ized objectives and under mild conditions, the method converges globally.
  arXiv  Detail & Related papers  (2022-01-28T05:53:28Z)
• Incomplete MaxSAT Approaches for Combinatorial Testing [0.0]
  We present a Satisfiability (SAT)-based approach for building Mixed Covering Arrays with Constraints of minimum length. This problem is central in Combinatorial Testing for the detection of system failures.
  arXiv  Detail & Related papers  (2021-05-26T14:00:56Z)
• Towards Optimally Efficient Tree Search with Deep Learning [76.64632985696237]
  This paper investigates the classical integer least-squares problem which estimates signals integer from linear models. The problem is NP-hard and often arises in diverse applications such as signal processing, bioinformatics, communications and machine learning. We propose a general hyper-accelerated tree search (HATS) algorithm by employing a deep neural network to estimate the optimal estimation for the underlying simplified memory-bounded A* algorithm.
  arXiv  Detail & Related papers  (2021-01-07T08:00:02Z)
• On Continuous Local BDD-Based Search for Hybrid SAT Solving [40.252804008544985]
  We propose a novel algorithm for efficiently computing the gradient needed by CLS. We study the capabilities and limitations of our versatile CLS solver, GradSAT, by applying it on many benchmark instances. The experimental results indicate that GradSAT can be a useful addition to the portfolio of existing SAT and MaxSAT solvers for solving Boolean satisfiability and optimization problems.
  arXiv  Detail & Related papers  (2020-12-14T22:36:20Z)
• Extreme Algorithm Selection With Dyadic Feature Representation [78.13985819417974]
  We propose the setting of extreme algorithm selection (XAS) where we consider fixed sets of thousands of candidate algorithms. We assess the applicability of state-of-the-art AS techniques to the XAS setting and propose approaches leveraging a dyadic feature representation.
  arXiv  Detail & Related papers  (2020-01-29T09:40:58Z)

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.