Efficient Parallel Algorithm for Decomposing Hard CircuitSAT Instances

• URL: http://arxiv.org/abs/2602.17130v1
• Date: Thu, 19 Feb 2026 07:05:48 GMT
• Title: Efficient Parallel Algorithm for Decomposing Hard CircuitSAT Instances
• Authors: Victor Kondratiev, Irina Gribanova, Alexander Semenov,
• Abstract summary: We propose a novel parallel algorithm for decomposing hard CircuitSAT instances.<n>Our approach is implemented as a parameterized parallel algorithm, where adjusting the parameters allows efficient identification of high-quality decompositions.
• Score: 44.0167033148715
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: We propose a novel parallel algorithm for decomposing hard CircuitSAT instances. The technique employs specialized constraints to partition an original SAT instance into a family of weakened formulas. Our approach is implemented as a parameterized parallel algorithm, where adjusting the parameters allows efficient identification of high-quality decompositions, guided by hardness estimations computed in parallel. We demonstrate the algorithm's practical efficacy on challenging CircuitSAT instances, including those encoding Logical Equivalence Checking of Boolean circuits and preimage attacks on cryptographic hash functions.

Related papers

• Block encoding of sparse matrices with a periodic diagonal structure [67.45502291821956]
  We provide an explicit quantum circuit for block encoding a sparse matrix with a periodic diagonal structure.<n>Various applications for the presented methodology are discussed in the context of solving differential problems.
  arXiv  Detail & Related papers  (2026-02-11T07:24:33Z)
• Stabilizer circuit verification [0.0]
  We propose a set of efficient classical algorithms to fully characterize and exhaustively verify stabilizer circuits. We provide an algorithm for checking the equivalence of stabilizer circuits. All of our algorithms provide relations of measurement outcomes among corresponding circuit representations.
  arXiv  Detail & Related papers  (2023-09-15T18:06:17Z)
• 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)
• Geometry-Aware Approaches for Balancing Performance and Theoretical Guarantees in Linear Bandits [5.847084649531299]
  Thompson sampling and Greedy demonstrate promising empirical performance, yet this contrasts with their pessimistic theoretical regret bounds.<n>We propose a new data-driven technique that tracks the geometric properties of the uncertainty ellipsoid around the main problem parameter.<n>This methodology enables us to formulate a data-driven frequentist regret bound, which incorporates the geometric information, for a broad class of base algorithms, including Greedy, OFUL, and Thompson sampling.
  arXiv  Detail & Related papers  (2023-06-26T17:38:45Z)
• FastDiagP: An Algorithm for Parallelized Direct Diagnosis [64.65251961564606]
  FastDiag is a typical direct diagnosis algorithm that supports diagnosis calculation without predetermining conflicts. We propose a novel algorithm, so-called FastDiagP, which is based on the idea of speculative programming. This mechanism helps to provide consistency checks with fast answers and boosts the algorithm's runtime performance.
  arXiv  Detail & Related papers  (2023-05-11T16:26:23Z)
• Quantum Algorithm for Path-Edge Sampling [0.9990687944474739]
  We present a quantum algorithm for sampling an edge on a path between two nodes s and t in an undirected graph given as an adjacency matrix. We use this path sampling algorithm as a subroutine for st-path finding and st-cut-set finding algorithms in some specific cases.
  arXiv  Detail & Related papers  (2023-03-06T17:45:12Z)
• 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)
• Accelerating ERM for data-driven algorithm design using output-sensitive techniques [26.32088674030797]
  We study techniques to develop efficient learning algorithms for data-driven algorithm design. Our approach involves two novel ingredients -- an output-sensitive algorithm for enumerating polytopes induced by a set of hyperplanes. We illustrate our techniques by giving algorithms for pricing problems, linkage-based clustering and dynamic-programming based sequence alignment.
  arXiv  Detail & Related papers  (2022-04-07T17:27:18Z)
• Temporal Parallelization of Inference in Hidden Markov Models [0.0]
  This paper presents algorithms for parallelization of inference in hidden Markov models (HMMs) We propose parallel backward-forward type of filtering and smoothing algorithm as well as parallel Viterbi-type maximum-a-posteriori (MAP) We empirically compare the performance of the proposed methods to classical methods on a highly parallel processing unit (GPU)
  arXiv  Detail & Related papers  (2021-02-10T21:26:09Z)
• Accelerated Message Passing for Entropy-Regularized MAP Inference [89.15658822319928]
  Maximum a posteriori (MAP) inference in discrete-valued random fields is a fundamental problem in machine learning. Due to the difficulty of this problem, linear programming (LP) relaxations are commonly used to derive specialized message passing algorithms. We present randomized methods for accelerating these algorithms by leveraging techniques that underlie classical accelerated gradient.
  arXiv  Detail & Related papers  (2020-07-01T18:43:32Z)
• Extreme Algorithm Selection With Dyadic Feature Representation [78.13985819417974]
  We propose the setting of extreme algorithm selection (XAS) where we consider fixed sets of thousands of candidate algorithms. We assess the applicability of state-of-the-art AS techniques to the XAS setting and propose approaches leveraging a dyadic feature representation.
  arXiv  Detail & Related papers  (2020-01-29T09:40:58Z)

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.