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

Using Monte Carlo Method for Searching Partitionings of Hard Variants of Boolean Satisfiability Problem

Тип публикации: Статья в журнале

Тип материала: Текст

Авторы: Semenov A., Zaikin O.

Журнал: Lecture Notes in Computer Science

Язык публикации: english

Том: 9251

Номера страниц: 221-230

Количество страниц: 10

Год публикации: 2015

Отчетный год: 2015

DOI: 10.1007/978-3-319-21909-7_21

Аннотация: In this paper we propose the approach for constructing partitionings of hard variants of the Boolean satisfiability problem (SAT). Such partitionings can be used for solving corresponding SAT instances in parallel. We suggest the approach based on the Monte Carlo method for estimating time of processing of an arbitrary partitioning. We solve the problem of search for a partitioning with good effectiveness via the optimization of the special predictive function over the finite search space. For this purpose we use the tabu search strategy. In our computational experiments we found partitionings for SAT instances encoding problems of inversion of some cryptographic functions. Several of these SAT instances with realistic predicted solving time were successfully solved on a computing cluster and in the volunteer computing project SAT@home. The solving time agrees well with estimations obtained by the proposed method.

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

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

Индексируется УБС: Нет

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

Индексируется ВАК: Нет

Индексируется CORE: Нет