Massively Parallel Continuous Local Search for Hybrid SAT Solving on GPUs

• URL: http://arxiv.org/abs/2308.15020v1
• Date: Tue, 29 Aug 2023 04:50:07 GMT
• Title: Massively Parallel Continuous Local Search for Hybrid SAT Solving on GPUs
• Authors: Yunuo Cen, Zhiwei Zhang, Xuanyao Fong
• Abstract summary: We propose FastFourierSAT, a highly parallel hybrid SAT solver based on gradient-driven continuous local search. Our results show that FastFourierSAT computes the gradient 100+ times faster than previous prototypes implemented on CPU. FastFourierSAT solves most instances and demonstrates promising performance on larger-size instances.
• Score: 5.245714076090567
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Although state-of-the-art (SOTA) SAT solvers based on conflict-driven clause learning (CDCL) have achieved remarkable engineering success, their sequential nature limits the parallelism that may be extracted for acceleration on platforms such as the graphics processing unit (GPU). In this work, we propose FastFourierSAT, a highly parallel hybrid SAT solver based on gradient-driven continuous local search (CLS). This is realized by a novel parallel algorithm inspired by the Fast Fourier Transform (FFT)-based convolution for computing the elementary symmetric polynomials (ESPs), which is the major computational task in previous CLS methods. The complexity of our algorithm matches the best previous result. Furthermore, the substantial parallelism inherent in our algorithm can leverage the GPU for acceleration, demonstrating significant improvement over the previous CLS approaches. We also propose to incorporate the restart heuristics in CLS to improve search efficiency. We compare our approach with the SOTA parallel SAT solvers on several benchmarks. Our results show that FastFourierSAT computes the gradient 100+ times faster than previous prototypes implemented on CPU. Moreover, FastFourierSAT solves most instances and demonstrates promising performance on larger-size instances.

Related papers

• Iterative quantum optimization of spin glass problems with rapidly oscillating transverse fields [0.0]
  We introduce a new iterative quantum algorithm, called Iterative Symphonic Tunneling for Satisfiability problems (IST-SAT) IST-SAT solves quantum spin glass optimization problems using high-frequency oscillating transverse fields.
  arXiv  Detail & Related papers  (2024-08-13T02:09:30Z)
• Sparsity-Constraint Optimization via Splicing Iteration [1.3622424109977902]
  We develop an algorithm named Sparsity-Constraint Optimization via sPlicing itEration (SCOPE) SCOPE converges effectively without tuning parameters. We apply SCOPE to solve quadratic optimization, learn sparse classifiers, and recover sparse Markov networks for binary variables. Our open-source Python package skscope based on C++ implementation is publicly available on GitHub.
  arXiv  Detail & Related papers  (2024-06-17T18:34:51Z)
• torchmSAT: A GPU-Accelerated Approximation To The Maximum Satisfiability Problem [1.5850859526672516]
  We derive a single differentiable function capable of approximating solutions for the Maximum Satisfiability Problem (MaxSAT) We present a novel neural network architecture to model our differentiable function, and progressively solve MaxSAT using backpropagation.
  arXiv  Detail & Related papers  (2024-02-06T02:33:00Z)
• Fast, Scalable, Warm-Start Semidefinite Programming with Spectral Bundling and Sketching [53.91395791840179]
  We present Unified Spectral Bundling with Sketching (USBS), a provably correct, fast and scalable algorithm for solving massive SDPs. USBS provides a 500x speed-up over the state-of-the-art scalable SDP solver on an instance with over 2 billion decision variables.
  arXiv  Detail & Related papers  (2023-12-19T02:27:22Z)
• Solving MaxSAT with Matrix Multiplication [15.349236934751897]
  We propose an algorithm for Maximum Satisfiability (MaxSAT) specifically designed to run on neural network accelerators such as GPUs and TPUs. Our approach, which we term RbmSAT, is a new design point in the algorithm-hardware co-design space for MaxSAT. We present timed results on a subset of problem instances from the annual MaxSAT Evaluations Incomplete Un Track for the years 2018 to 2021.
  arXiv  Detail & Related papers  (2023-11-01T14:46:46Z)
• Stochastic Optimization for Non-convex Problem with Inexact Hessian Matrix, Gradient, and Function [99.31457740916815]
  Trust-region (TR) and adaptive regularization using cubics have proven to have some very appealing theoretical properties. We show that TR and ARC methods can simultaneously provide inexact computations of the Hessian, gradient, and function values.
  arXiv  Detail & Related papers  (2023-10-18T10:29:58Z)
• High Performance Computing Applied to Logistic Regression: A CPU and GPU Implementation Comparison [0.0]
  We present a versatile GPU-based parallel version of Logistic Regression (LR) Our implementation is a direct translation of the parallel Gradient Descent Logistic Regression algorithm proposed by X. Zou et al. Our method is particularly advantageous for real-time prediction applications like image recognition, spam detection, and fraud detection.
  arXiv  Detail & Related papers  (2023-08-19T14:49:37Z)
• Matching Pursuit Based Scheduling for Over-the-Air Federated Learning [67.59503935237676]
  This paper develops a class of low-complexity device scheduling algorithms for over-the-air learning via the method of federated learning. Compared to the state-of-the-art proposed scheme, the proposed scheme poses a drastically lower efficiency system. The efficiency of the proposed scheme is confirmed via experiments on the CIFAR dataset.
  arXiv  Detail & Related papers  (2022-06-14T08:14:14Z)
• AsySQN: Faster Vertical Federated Learning Algorithms with Better Computation Resource Utilization [159.75564904944707]
  We propose an asynchronous quasi-Newton (AsySQN) framework for vertical federated learning (VFL) The proposed algorithms make descent steps scaled by approximate without calculating the inverse Hessian matrix explicitly. We show that the adopted asynchronous computation can make better use of the computation resource.
  arXiv  Detail & Related papers  (2021-09-26T07:56:10Z)
• 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)
• Accelerating Feedforward Computation via Parallel Nonlinear Equation Solving [106.63673243937492]
  Feedforward computation, such as evaluating a neural network or sampling from an autoregressive model, is ubiquitous in machine learning. We frame the task of feedforward computation as solving a system of nonlinear equations. We then propose to find the solution using a Jacobi or Gauss-Seidel fixed-point method, as well as hybrid methods of both. Our method is guaranteed to give exactly the same values as the original feedforward computation with a reduced (or equal) number of parallelizable iterations, and hence reduced time given sufficient parallel computing power.
  arXiv  Detail & Related papers  (2020-02-10T10:11:31Z)

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.