Using Parallel SAT Solving to Study Hard Combinatorial Problems Associated with Boolean Circuits

We propose a family of parallel algorithms aimed at solving problems related to hardware verification. We consider the Logical Equivalence Checking problem (LEC) and a particular case known as Automated Test Pattern Generation (ATPG). The main algorithmic basis for solving LEC and ATPG consists of state-of-the-art SAT-solving algorithms. However, for extremely hard SAT instances, the situation often arises when we can say nothing about the runtime of the SAT solver on a considered instance. We can, nonetheless, estimate the runtime if we decompose the original instance into a family of simpler instances that can be solved in a reasonable time. As an additional bonus, this approach provides a means for solving a given problem in parallel. We exploit the described idea in some extremely hard ATPG instances in SAT form and demonstrate that parallel computing is essential for efficient ATPG solving.