Black-Box Optimization in an Extended Search Space for SAT Solving

The Divide-and-Conquer approach is often used to solve hard instances of the Boolean satisfiability problem (SAT). In particular, it implies splitting an original SAT instance into a series of simpler subproblems. If this split satisfies certain conditions, then it is possible to use a stochastic pseudo-Boolean black-box function to estimate the time required for solving an original SAT instance with the chosen decomposition. One can use black-box optimization methods to minimize the function over the space of all possible decompositions. In the present study, we make use of peculiar features which stem from the NP-completeness of the Boolean satisfiability problem to improve this general approach. In particular, we show that the search space over which the black-box function is minimized can be extended by adding solver parameters and the SAT encoding parameters into it. In the computational experiments, we use the SMAC algorithm to optimize such black-box functions for hard SAT instances encoding the problems of cryptanalysis of several stream ciphers. The results show that the proposed approach outperforms the competition.