Large-block parallelism technology in sat problems

A new approach to SAT problems solution based on large-block parallelism concept incident to many high dimensionality problems is proposed. In this framework, the decomposition of the initial conjuctive normal form (CNF) to a CNF family is built with subsequent SAT problem solution for each CNF of the family on each computational node of the cluster. The planning of the optimal computation is done by optimizing a special predictive function. The efficiency of the approach is proved by solving cryptanalysis problems for summing and threshold generators.