Victor Kondratiev, Irina Gribanova, Alexander Semenov
The paper presents a new parallel algorithm that efficiently decomposes hard CircuitSAT instances by partitioning them into weaker formulas using specialized constraints.
This research introduces a new method to tackle difficult CircuitSAT problems, which are a type of computational problem related to verifying the correctness of circuits and cryptographic functions. The method works by breaking down the original problem into smaller, more manageable parts using a parallel computing approach. By adjusting certain settings, the algorithm can efficiently find the best way to decompose these problems, making it easier to solve them. The researchers tested their method on complex problems related to circuit verification and cryptography, showing its effectiveness.
