Solving MaxSAT with Matrix Multiplication

• URL: http://arxiv.org/abs/2311.02101v1
• Date: Wed, 1 Nov 2023 14:46:46 GMT
• Title: Solving MaxSAT with Matrix Multiplication
• Authors: David Warde-Farley, Vinod Nair, Yujia Li, Ivan Lobov, Felix Gimeno, Simon Osindero
• Abstract summary: 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.
• Score: 15.349236934751897
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: We propose an incomplete algorithm for Maximum Satisfiability (MaxSAT) specifically designed to run on neural network accelerators such as GPUs and TPUs. Given a MaxSAT problem instance in conjunctive normal form, our procedure constructs a Restricted Boltzmann Machine (RBM) with an equilibrium distribution wherein the probability of a Boolean assignment is exponential in the number of clauses it satisfies. Block Gibbs sampling is used to stochastically search the space of assignments with parallel Markov chains. Since matrix multiplication is the main computational primitive for block Gibbs sampling in an RBM, our approach leads to an elegantly simple algorithm (40 lines of JAX) well-suited for neural network accelerators. Theoretical results about RBMs guarantee that the required number of visible and hidden units of the RBM scale only linearly with the number of variables and constant-sized clauses in the MaxSAT instance, ensuring that the computational cost of a Gibbs step scales reasonably with the instance size. Search throughput can be increased by batching parallel chains within a single accelerator as well as by distributing them across multiple accelerators. As a further enhancement, a heuristic based on unit propagation running on CPU is periodically applied to the sampled assignments. 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 Evaluation's Incomplete Unweighted Track for the years 2018 to 2021. When allotted the same running time and CPU compute budget (but no TPUs), RbmSAT outperforms other participating solvers on problems drawn from three out of the four years' competitions. Given the same running time on a TPU cluster for which RbmSAT is uniquely designed, it outperforms all solvers on problems drawn from all four years.

Related papers

• 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)
• Grover-QAOA for 3-SAT: Quadratic Speedup, Fair-Sampling, and Parameter Clustering [6.86850788361785]
  This study shows numerical evidence for a quadratic speedup of the Grover Quantum Approximate Optimization Algorithm (G-QAOA) over random sampling. G-QAOA is less resource-intensive and more adaptable for 3-SAT and Max-SAT than Grover's algorithm, and it surpasses conventional QAOA in its ability to sample all solutions. We also observe G-QAOA advantages on the IonQ Aria quantum computer for small instances, finding that current hardware suffices to determine and sample all solutions.
  arXiv  Detail & Related papers  (2024-02-04T19:01:27Z)
• Massively Parallel Continuous Local Search for Hybrid SAT Solving on GPUs [5.245714076090567]
  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.
  arXiv  Detail & Related papers  (2023-08-29T04:50:07Z)
• Approximating a RUM from Distributions on k-Slates [88.32814292632675]
  We find a generalization-time algorithm that finds the RUM that best approximates the given distribution on average. Our theoretical result can also be made practical: we obtain a that is effective and scales to real-world datasets.
  arXiv  Detail & Related papers  (2023-05-22T17:43:34Z)
• Towards Tackling MaxSAT by Combining Nested Monte Carlo with Local Search [10.70006528984961]
  We introduce two algorithmic variations over UCTMAXSAT. First, a nesting of the tree search inspired by the Nested Monte Carlo Search algorithm is effective on most instance types in the benchmark. Second, we observe that using a static flip limit in SLS, the ideal budget depends heavily on the instance size and we propose to set it dynamically.
  arXiv  Detail & Related papers  (2023-02-26T03:37: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)
• Unfolding Projection-free SDP Relaxation of Binary Graph Classifier via GDPA Linearization [59.87663954467815]
  Algorithm unfolding creates an interpretable and parsimonious neural network architecture by implementing each iteration of a model-based algorithm as a neural layer. In this paper, leveraging a recent linear algebraic theorem called Gershgorin disc perfect alignment (GDPA), we unroll a projection-free algorithm for semi-definite programming relaxation (SDR) of a binary graph. Experimental results show that our unrolled network outperformed pure model-based graph classifiers, and achieved comparable performance to pure data-driven networks but using far fewer parameters.
  arXiv  Detail & Related papers  (2021-09-10T07:01:15Z)
• 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)
• Computationally efficient sparse clustering [67.95910835079825]
  We provide a finite sample analysis of a new clustering algorithm based on PCA. We show that it achieves the minimax optimal misclustering rate in the regime $|theta infty$.
  arXiv  Detail & Related papers  (2020-05-21T17:51:30Z)
• MPLP++: Fast, Parallel Dual Block-Coordinate Ascent for Dense Graphical Models [96.1052289276254]
  This work introduces a new MAP-solver, based on the popular Dual Block-Coordinate Ascent principle. Surprisingly, by making a small change to the low-performing solver, we derive the new solver MPLP++ that significantly outperforms all existing solvers by a large margin.
  arXiv  Detail & Related papers  (2020-04-16T16:20:53Z)

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.