arXiv · 2602.17130
Efficient Parallel Algorithm for Decomposing Hard CircuitSAT Instances
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.
Explore related subjects
Keep this discovery
Victor Kondratiev, Irina Gribanova, Alexander Semenov. 2026-02-19. Efficient Parallel Algorithm for Decomposing Hard CircuitSAT Instances. https://arxiv.org/abs/2602.17130
Cite the original work for its findings. Save a collection to share your selection of sources.