NLocalSAT: Boosting Local Search with Solution Prediction

• URL: http://arxiv.org/abs/2001.09398v4
• Date: Wed, 9 Dec 2020 07:01:26 GMT
• Title: NLocalSAT: Boosting Local Search with Solution Prediction
• Authors: Wenjie Zhang, Zeyu Sun, Qihao Zhu, Ge Li, Shaowei Cai, Yingfei Xiong, and Lu Zhang
• Abstract summary: An effective way for solving a satisfiable SAT problem is the local search (SLS) This method is assigned in a random manner, which impacts the effectiveness of SLS solvers. NLocalSAT combines SLS with a solution prediction model, which boosts SLS by changing initialization assignments with a neural network. Experiments show that solvers with NLocalSAT achieve 27% 62% improvement over the original SLS solvers.
• Score: 36.69915361918781
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: The Boolean satisfiability problem (SAT) is a famous NP-complete problem in computer science. An effective way for solving a satisfiable SAT problem is the stochastic local search (SLS). However, in this method, the initialization is assigned in a random manner, which impacts the effectiveness of SLS solvers. To address this problem, we propose NLocalSAT. NLocalSAT combines SLS with a solution prediction model, which boosts SLS by changing initialization assignments with a neural network. We evaluated NLocalSAT on five SLS solvers (CCAnr, Sparrow, CPSparrow, YalSAT, and probSAT) with instances in the random track of SAT Competition 2018. The experimental results show that solvers with NLocalSAT achieve 27% ~ 62% improvement over the original SLS solvers.

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. 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)
• SibylSat: Using SAT as an Oracle to Perform a Greedy Search on TOHTN Planning [2.2276906461400054]
  This paper presents SibylSat, a novel SAT-based method designed to efficiently solve totally-ordered HTN problems (TOHTN) In contrast to prevailing SAT-based HTN planners that employ a breadth-first search strategy, SibylSat adopts a greedy search approach, enabling it to identify promising decompositions for expansion. Our experimental evaluations demonstrate that SibylSat outperforms existing SAT-based TOHTN approaches in terms of both runtime and plan quality on most of the IPC benchmarks.
  arXiv  Detail & Related papers  (2024-11-04T12:37:59Z)
• Decomposing Hard SAT Instances with Metaheuristic Optimization [52.03315747221343]
  We introduce the notion of decomposition hardness (d-hardness) We show that the d-hardness expresses an estimate of the hardness of $C$ w.r.t.
  arXiv  Detail & Related papers  (2023-12-16T12:44:36Z)
• G4SATBench: Benchmarking and Advancing SAT Solving with Graph Neural Networks [7.951021955925275]
  Graph neural networks (GNNs) have emerged as a promising approach for solving the Boolean Satisfiability Problem (SAT) G4SATBench is the first benchmark study that establishes a comprehensive evaluation framework for GNN-based SAT solvers. Our results provide valuable insights into the performance of GNN-based SAT solvers.
  arXiv  Detail & Related papers  (2023-09-29T02:50:57Z)
• A hybrid Quantum proposal to deal with 3-SAT problem [75.38606213726906]
  This paper presents and describes a hybrid quantum computing strategy for solving 3-SAT problems. The performance of this approximation has been tested over a set of representative scenarios when dealing with 3-SAT from the quantum computing perspective.
  arXiv  Detail & Related papers  (2023-06-07T12:19:22Z)
• Addressing Variable Dependency in GNN-based SAT Solving [19.38746341365531]
  We propose AsymSAT, a GNN-based architecture which integrates recurrent neural networks to generate dependent predictions for variable assignments. Experiment results show that dependent variable prediction extends the solving capability of the GNN-based method as it improves the number of solved SAT instances on large test sets.
  arXiv  Detail & Related papers  (2023-04-18T05:33:33Z)
• Estimating the hardness of SAT encodings for Logical Equivalence Checking of Boolean circuits [58.83758257568434]
  We show that the hardness of SAT encodings for LEC instances can be estimated textitw.r.t some SAT partitioning. The paper proposes several methods for constructing partitionings, which, when used in practice, allow one to estimate the hardness of SAT encodings for LEC with good accuracy.
  arXiv  Detail & Related papers  (2022-10-04T09:19:13Z)
• SATformer: Transformer-Based UNSAT Core Learning [0.0]
  This paper introduces SATformer, a Transformer-based approach for the Boolean Satisfiability (SAT) problem. Rather than solving the problem directly, SATformer approaches the problem from the opposite direction by focusing on unsatisfiability. SATformer is trained through a multi-task learning approach, using the single-bit satisfiability result and the minimal unsatisfiable core. Experimental results show that our SATformer can decrease the runtime of existing solvers by an average of 21.33%.
  arXiv  Detail & Related papers  (2022-09-02T11:17:39Z)
• Machine Learning Methods in Solving the Boolean Satisfiability Problem [72.21206588430645]
  The paper reviews the recent literature on solving the Boolean satisfiability problem (SAT) with machine learning techniques. We examine the evolving ML-SAT solvers from naive classifiers with handcrafted features to the emerging end-to-end SAT solvers such as NeuroSAT.
  arXiv  Detail & Related papers  (2022-03-02T05:14:12Z)
• Transformer-based Machine Learning for Fast SAT Solvers and Logic Synthesis [63.53283025435107]
  CNF-based SAT and MaxSAT solvers are central to logic synthesis and verification systems. In this work, we propose a one-shot model derived from the Transformer architecture to solve the MaxSAT problem.
  arXiv  Detail & Related papers  (2021-07-15T04:47:35Z)
• Improving probability selecting based weights for Satisfiability Problem [6.59413630027528]
  We present a new SLS algorithm named SelectNTS for uniform random k-SAT and HRS. Our algorithm outperforms state-of-the-art random SAT algorithms, and our SelectNTS can effectively solve both uniform random k-SAT and HRS.
  arXiv  Detail & Related papers  (2020-07-30T02:23:07Z)

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.