torchmSAT: A GPU-Accelerated Approximation To The Maximum Satisfiability Problem

• URL: http://arxiv.org/abs/2402.03640v1
• Date: Tue, 6 Feb 2024 02:33:00 GMT
• Title: torchmSAT: A GPU-Accelerated Approximation To The Maximum Satisfiability Problem
• Authors: Abdelrahman Hosny, Sherief Reda
• Abstract summary: 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.
• Score: 1.5850859526672516
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: The remarkable achievements of machine learning techniques in analyzing discrete structures have drawn significant attention towards their integration into combinatorial optimization algorithms. Typically, these methodologies improve existing solvers by injecting learned models within the solving loop to enhance the efficiency of the search process. In this work, we derive a single differentiable function capable of approximating solutions for the Maximum Satisfiability Problem (MaxSAT). Then, we present a novel neural network architecture to model our differentiable function, and progressively solve MaxSAT using backpropagation. This approach eliminates the need for labeled data or a neural network training phase, as the training process functions as the solving algorithm. Additionally, we leverage the computational power of GPUs to accelerate these computations. Experimental results on challenging MaxSAT instances show that our proposed methodology outperforms two existing MaxSAT solvers, and is on par with another in terms of solution cost, without necessitating any training or access to an underlying SAT solver. Given that numerous NP-hard problems can be reduced to MaxSAT, our novel technique paves the way for a new generation of solvers poised to benefit from neural network GPU acceleration.

Related papers

• Optimizing Solution-Samplers for Combinatorial Problems: The Landscape of Policy-Gradient Methods [52.0617030129699]
  We introduce a novel theoretical framework for analyzing the effectiveness of DeepMatching Networks and Reinforcement Learning methods. Our main contribution holds for a broad class of problems including Max-and Min-Cut, Max-$k$-Bipartite-Bi, Maximum-Weight-Bipartite-Bi, and Traveling Salesman Problem. As a byproduct of our analysis we introduce a novel regularization process over vanilla descent and provide theoretical and experimental evidence that it helps address vanishing-gradient issues and escape bad stationary points.
  arXiv  Detail & Related papers  (2023-10-08T23:39:38Z)
• Are Graph Neural Networks Optimal Approximation Algorithms? [26.5364112420121]
  We design graph neural network architectures that capture optimal approximation algorithms for a class of optimization problems. We take advantage of OptGNN's ability to capture convex relaxations to design an algorithm for producing bounds on the optimal solution from the learned embeddings of OptGNN.
  arXiv  Detail & Related papers  (2023-10-01T00:12:31Z)
• Training Neural Networks using SAT solvers [1.0152838128195465]
  We propose an algorithm to explore the global optimisation method, using SAT solvers, for training a neural net. In the experiments, we demonstrate the effectiveness of our algorithm against the ADAM optimiser in certain tasks like parity learning.
  arXiv  Detail & Related papers  (2022-06-10T01:31:12Z)
• 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)
• ML Supported Predictions for SAT Solvers Performance [0.0]
  Internal solver runtime parameters have been collected and analyzed. A machine learning model has been created for the binary classification of the solver's termination behavior.
  arXiv  Detail & Related papers  (2021-12-17T11:17:29Z)
• 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)
• 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)
• Learning from Survey Propagation: a Neural Network for MAX-E-$3$-SAT [0.0]
  This paper presents a new algorithm for computing approximate solutions in $Theta(N)$ for the Maximum Exact 3-Satisfiability (MAX-E-$3$-SAT) problem.
  arXiv  Detail & Related papers  (2020-12-10T07:59:54Z)
• Communication-Efficient Distributed Stochastic AUC Maximization with Deep Neural Networks [50.42141893913188]
  We study a distributed variable for large-scale AUC for a neural network as with a deep neural network. Our model requires a much less number of communication rounds and still a number of communication rounds in theory. Our experiments on several datasets show the effectiveness of our theory and also confirm our theory.
  arXiv  Detail & Related papers  (2020-05-05T18:08:23Z)
• Physarum Powered Differentiable Linear Programming Layers and Applications [48.77235931652611]
  We propose an efficient and differentiable solver for general linear programming problems. We show the use of our solver in a video segmentation task and meta-learning for few-shot learning.
  arXiv  Detail & Related papers  (2020-04-30T01:50:37Z)

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.