High-Throughput SAT Sampling

• URL: http://arxiv.org/abs/2502.08673v1
• Date: Wed, 12 Feb 2025 03:20:45 GMT
• Title: High-Throughput SAT Sampling
• Authors: Arash Ardakani, Minwoo Kang, Kevin He, Qijing Huang, John Wawrzynek,
• Abstract summary: We present a novel technique for GPU-accelerated satisfiability (SAT) sampling. Our method transforms the logical constraints of SAT problems by factoring their CNF representations into simplified multi-level, multi-output Boolean functions. We achieve GPU-accelerated sampling with significant improvements ranging from $33.6times$ to $523.6times$ over state-of-the-art samplers.
• Score: 3.8108678341258138
• License:
• Abstract: In this work, we present a novel technique for GPU-accelerated Boolean satisfiability (SAT) sampling. Unlike conventional sampling algorithms that directly operate on conjunctive normal form (CNF), our method transforms the logical constraints of SAT problems by factoring their CNF representations into simplified multi-level, multi-output Boolean functions. It then leverages gradient-based optimization to guide the search for a diverse set of valid solutions. Our method operates directly on the circuit structure of refactored SAT instances, reinterpreting the SAT problem as a supervised multi-output regression task. This differentiable technique enables independent bit-wise operations on each tensor element, allowing parallel execution of learning processes. As a result, we achieve GPU-accelerated sampling with significant runtime improvements ranging from $33.6\times$ to $523.6\times$ over state-of-the-art heuristic samplers. We demonstrate the superior performance of our sampling method through an extensive evaluation on $60$ instances from a public domain benchmark suite utilized in previous studies.

Related papers

• 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. While cube-and-conquer has proven successful for pure SAT problems, its application to SAT solvers extended with propagators presents unique challenges. 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)
• Quasi-random Multi-Sample Inference for Large Language Models [1.647759094903376]
  Large language models (LLMs) are often equipped with multi-sample decoding strategies. Traditional text generation methods, such as beam search and sampling-based techniques, have notable limitations. This study explores the potential of arithmetic sampling, contrasting it with ancestral sampling.
  arXiv  Detail & Related papers  (2024-11-09T18:55:04Z)
• Provably Faster Algorithms for Bilevel Optimization via Without-Replacement Sampling [96.47086913559289]
  gradient-based algorithms are widely used in bilevel optimization. We introduce a without-replacement sampling based algorithm which achieves a faster convergence rate. We validate our algorithms over both synthetic and real-world applications.
  arXiv  Detail & Related papers  (2024-11-07T17:05:31Z)
• Resource-Constrained Heuristic for Max-SAT [0.848762374187855]
  We propose a resource-constrained for instances of Max-SAT that iteratively decomposes a larger problem into smaller subcomponents. We analyze a set of variable selection methods, including a novel graph-based method that exploits the structure of a given SAT instance. We demonstrate our results on a set of randomly generated Max-SAT instances as well as real world examples from the Max-SAT evaluation benchmarks.
  arXiv  Detail & Related papers  (2024-10-11T18:20:08Z)
• 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)
• 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)
• Multi-block-Single-probe Variance Reduced Estimator for Coupled Compositional Optimization [49.58290066287418]
  We propose a novel method named Multi-block-probe Variance Reduced (MSVR) to alleviate the complexity of compositional problems. Our results improve upon prior ones in several aspects, including the order of sample complexities and dependence on strongity.
  arXiv  Detail & Related papers  (2022-07-18T12:03:26Z)
• Fast Differentiable Matrix Square Root and Inverse Square Root [65.67315418971688]
  We propose two more efficient variants to compute the differentiable matrix square root and the inverse square root. For the forward propagation, one method is to use Matrix Taylor Polynomial (MTP), and the other method is to use Matrix Pad'e Approximants (MPA) A series of numerical tests show that both methods yield considerable speed-up compared with the SVD or the NS iteration.
  arXiv  Detail & Related papers  (2022-01-29T10:00:35Z)
• 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)
• 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)
• Non-Adaptive Adaptive Sampling on Turnstile Streams [57.619901304728366]
  We give the first relative-error algorithms for column subset selection, subspace approximation, projective clustering, and volume on turnstile streams that use space sublinear in $n$. Our adaptive sampling procedure has a number of applications to various data summarization problems that either improve state-of-the-art or have only been previously studied in the more relaxed row-arrival model.
  arXiv  Detail & Related papers  (2020-04-23T05:00:21Z)

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.