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

ABSTRACT

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.

KEYWORDS:

• Pseudo-Boolean optimization
• black-box optimization
• Monte-Carlo method
• SAT
• divide-and-conquer
• cryptanalysis

Acknowledgements

We thank anonymous reviewers for their thoughtful and constructive comments that made it possible to significantly improve the quality of the present paper. We also thank Dr Alexander Semenov for valuable preliminary discussions.

Disclosure statement

No potential conflict of interest was reported by the authors.

Additional information

Funding

The research was partially supported by the Council for Grants of the President of the Russian Federation (grant no. MK-4155.2018.9, stipend SP-2017.2019.5) and by the Russian Foundation for Basic Research (grant no. 19-07-00746-a).

Notes on contributors

O. S. Zaikin

O. S. Zaikin received his PhD in Computer Science from Tomsk State University, Russia in 2009. He is currently a leading researcher at Matrosov Institute for System Dynamics and Control Theory of Siberian Branch of Russian Academy of Sciences, Russia. His research interests include the Boolean satisfiability problem, global optimization, parallel computing, and cryptanalysis.

S. E. Kochemazov

S. E. Kochemazov is a researcher at the Matrosov Institute for System Dynamics and Control Theory of Siberian Branch of Russian Academy of Sciences, Russia. His major scientific interests are the Boolean satisfiability problem and algorithms for its solving, and the applications of high-performance computing for tackling hard combinatorial problems.