Application of the Monte Carlo method for estimating the total time of solving the SAT problem in parallel

The application of the Monte Carlo method to plan the solving process for hard examples of the Boolean satisfiability problem (SAT) on parallel computing systems is discussed. The parallelization of the SAT problem is reached as a result of choosing the subset of the set of variables of an original CNF (Conjunctive Normal Form). This set is called a decomposition set. For such sets, we can naturally define a number of parameters to measure the “quality” of decomposition. In order to evaluate these parameters, we use the computational scheme based on the Monte Carlo method. In particular, this method is used to search for the decomposition set with minimal predicted time of solving the original problem. Using the implemented parallel MPI-program, it is possible to obtain a prediction of time required to perform the logical cryptanalysis of the Bivium cipher on a computing cluster. We successfully performed the logical cryptanalysis of several weakened versions of the Bivium cipher. The computing cost of such a cryptanalysis is in agreement with the predicted one.