Efficient Parallel Algorithm for Decomposing Hard CircuitSAT Instances
Not on the map. Why?
Abstract (arXiv)
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.
Key facts. No citing papers in the map yet (data through 14 Oct 2026). Builds on 5 of its 47 references that are in the map. First posted on arXiv 19 Feb 2026.
Builds on
5 of 47 references.
References · 5
- 2018On Cryptographic Attacks Using Backdoors for SATcited by 6
- 2018Using Automatic Generation of Relaxation Constraints to Improve the Preimage Attack on 39-step MD4cited by 3
- 2018Translation of Algorithmic Descriptions of Discrete Functions to SAT with Applications to Cryptanalysis Problemscited by 3
- 2022Inverting Cryptographic Hash Functions via Cube-and-Conquercited by 1
- 2023Decomposing Hard SAT Instances with Metaheuristic Optimizationcited by 1
Built on by
Not cited yet.