Efficient Parallel Algorithm for Decomposing Hard CircuitSAT Instances

TL;DR

This paper introduces a new parallel algorithm that efficiently decomposes complex CircuitSAT problems by partitioning them into simpler formulas, enabling faster solving of challenging instances such as cryptographic and logical verification tasks.

Contribution

The paper presents a novel parameterized parallel decomposition algorithm for CircuitSAT, utilizing specialized constraints and hardness estimations for improved efficiency.

Findings

Effective decomposition of hard CircuitSAT instances demonstrated

Applicable to cryptographic hash preimage attacks and circuit equivalence checking

Parallel approach reduces computational complexity and runtime

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.