Advancing Stochastic 3-SAT Solvers by Dissipating Oversatisfied Constraints

• URL: http://arxiv.org/abs/2506.15774v1
• Date: Wed, 18 Jun 2025 18:00:01 GMT
• Title: Advancing Stochastic 3-SAT Solvers by Dissipating Oversatisfied Constraints
• Authors: J. Schwardt, J. C. Budich,
• Abstract summary: We introduce and benchmark a local search for the NP-complete satisfiability problem 3-SAT.<n>Our construction is based on the crucial observation that well established previous approaches such as WalkSAT are prone to get stuck in local minima.<n>We analyze and benchmark our algorithm on a randomly generated sample of hard but satisfiable 3-SAT instances with varying problem sizes up to N=15000.
• Score: 0.0
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: We introduce and benchmark a stochastic local search heuristic for the NP-complete satisfiability problem 3-SAT that drastically outperforms existing solvers in the notoriously difficult realm of critically hard instances. Our construction is based on the crucial observation that well established previous approaches such as WalkSAT are prone to get stuck in local minima that are distinguished from true solutions by a larger number of oversatisfied combinatorial constraints. To address this issue, the proposed algorithm, coined DOCSAT, dissipates oversatisfied constraints (DOC), i.e. reduces their unfavorable abundance so as to render them critical. We analyze and benchmark our algorithm on a randomly generated sample of hard but satisfiable 3-SAT instances with varying problem sizes up to N=15000. Quite remarkably, we find that DOCSAT outperforms both WalkSAT and other well known algorithms including the complete solver Kissat, even when comparing its ability to solve the hardest quintile of the sample to the average performance of its competitors. The essence of DOCSAT may be seen as a way of harnessing statistical structure beyond the primary cost function of a combinatorial problem to avoid or escape local minima traps in stochastic local search, which opens avenues for generalization to other optimization problems.

Related papers

• Noise to the Rescue: Escaping Local Minima in Neurosymbolic Local Search [50.24983453990065]
  We show that applying BP to Godel logic, which represents conjunction and disjunction as min and max, is equivalent to a local search algorithm for SAT solving.<n>We propose the Godel Trick, which adds noise to the model's logits to escape local optima.
  arXiv  Detail & Related papers  (2025-03-03T18:42:13Z)
• Smart Cubing for Graph Search: A Comparative Study [15.989407883187962]
  Parallel solving via cube-and-conquer is a key method for scaling SAT solvers to hard instances.<n>While cube-and-conquer has proven successful for pure SAT problems, its application to SAT solvers extended with propagators presents unique challenges.<n>We study this problem using SAT Modulo Symmetries (SMS) as our primary test case, where a symmetry-breaking propagator reduces the search space by learning constraints that eliminate isomorphic graphs.
  arXiv  Detail & Related papers  (2025-01-27T22:15:54Z)
• 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)
• 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)
• Using deep learning to construct stochastic local search SAT solvers with performance bounds [0.0]
  We train oracles using Graph Neural Networks and evaluate them on two SLS solvers on random SAT instances of varying difficulty. We find that access to GNN-based oracles significantly boosts the performance of both solvers.
  arXiv  Detail & Related papers  (2023-09-20T16:27:52Z)
• Amplitude amplification-inspired QAOA: Improving the success probability for solving 3SAT [55.78588835407174]
  The amplitude amplification algorithm can be applied to unstructured search for satisfying variable assignments. The Quantum Approximate Optimization Algorithm (QAOA) is a promising candidate for solving 3SAT for Noisy Intermediate-Scale Quantum devices. We introduce amplitude amplification-inspired variants of QAOA to improve the success probability for 3SAT.
  arXiv  Detail & Related papers  (2023-03-02T11:52:39Z)
• Outlier-Robust Sparse Estimation via Non-Convex Optimization [73.18654719887205]
  We explore the connection between high-dimensional statistics and non-robust optimization in the presence of sparsity constraints. We develop novel and simple optimization formulations for these problems. As a corollary, we obtain that any first-order method that efficiently converges to station yields an efficient algorithm for these tasks.
  arXiv  Detail & Related papers  (2021-09-23T17:38:24Z)
• 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)
• 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)
• Adaptive Sampling for Best Policy Identification in Markov Decision Processes [79.4957965474334]
  We investigate the problem of best-policy identification in discounted Markov Decision (MDPs) when the learner has access to a generative model. The advantages of state-of-the-art algorithms are discussed and illustrated.
  arXiv  Detail & Related papers  (2020-09-28T15:22:24Z)
• Beyond Worst-Case Analysis in Stochastic Approximation: Moment Estimation Improves Instance Complexity [58.70807593332932]
  We study oracle complexity of gradient based methods for approximation problems. We focus on instance-dependent complexity instead of worst case complexity. Our proposed algorithm and its analysis provide a theoretical justification for the success of moment estimation.
  arXiv  Detail & Related papers  (2020-06-08T09:25:47Z)

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.