On black-box optimization in divide-and-conquer SAT solving.

Solving hard instances of the Boolean satisfiability problem (SAT) in practice is an interestingly nontrivial area. The heuristic nature of SAT solvers makes it impossible to know in advance how long it will take to solve any particular SAT instance. One way of coping with this disadvantage is the Divide-and-Conquer approach when an original SAT instance is decomposed into a set of simpler subproblems. However, the way it is decomposed plays a crucial role in the resulting effectiveness of solving. In the present study, we reduce the problem of choosing a proper decomposition to a stochastic pseudo-Boolean black-box optimization problem. Several optimization algorithms of different types were used to analyse a number of hard SAT-based optimization problems, related to SAT-based cryptanalysis of state-of-the-art stream ciphers. A meticulous computational study showed that some of the considered optimization algorithms perform much better than the others in the context of the problems from the considered class. It turned out that the obtained results also pose some cryptographic interest.