Страница публикации

Black-box optimization in an extended search space for sat solving

Авторы: Zaikin O., Kochemazov S.

Журнал: CEUR Workshop Proceedings: Proc. of the 18th Intern. Conf. on Mathematical Optimization Theory and Operations Research (MOTOR'2019; Ekaterinburg)

Том: 11548


Год: 2019

Отчётный год: 2019


Местоположение издательства:


Аннотация: 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.

Индексируется WOS: 1

Индексируется Scopus: 1

Индексируется РИНЦ: 1

Публикация в печати: 0

Добавил в систему: