Search papers, labs, and topics across Lattice.
The paper introduces a parallel algorithm for decomposing hard CircuitSAT instances by partitioning them into weakened formulas using specialized constraints. This decomposition enables more efficient solving of complex SAT problems by breaking them into smaller, more manageable subproblems. Experiments on CircuitSAT instances encoding logical equivalence checking and cryptographic hash function preimage attacks demonstrate the practical effectiveness of the algorithm.
Breaking down notoriously hard CircuitSAT problems just got easier: a new parallel decomposition algorithm efficiently weakens formulas, paving the way for faster solutions.
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.
