# Efficient Parallel Algorithm for Decomposing Hard CircuitSAT Instances

arXiv: https://arxiv.org/abs/2602.17130 · HTML: https://mlsanity.com/paper/2602.17130/

## 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 (most cited first, 5 of 5)

- [On Cryptographic Attacks Using Backdoors for SAT](https://mlsanity.com/paper/1803.04646/) (2018)
- [Using Automatic Generation of Relaxation Constraints to Improve the Preimage Attack on 39-step MD4](https://mlsanity.com/paper/1802.06940/) (2018)
- [Translation of Algorithmic Descriptions of Discrete Functions to SAT with Applications to Cryptanalysis Problems](https://mlsanity.com/paper/1805.07239/) (2018)
- [Inverting Cryptographic Hash Functions via Cube-and-Conquer](https://mlsanity.com/paper/2212.02405/) (2022)
- [Decomposing Hard SAT Instances with Metaheuristic Optimization](https://mlsanity.com/paper/2312.10436/) (2023)

## 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.