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

Дубликаты конфликтных ограничений в CDCL-выводе и их использование в задачах обращения некоторых криптографических функций

Авторы: Кондратьев В.С., Семенов А.А., Заикин О.С.

Журнал: Вычисл. методы и программирование: новые вычисл. технологии

Том: 20

Номер: 1

Год: 2019

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

Издательство:

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

URL:

Проекты:

DOI: DOI: 10.26089/NumMet.v20r106

Аннотация: Изучен феномен повторного порождения конфликтных ограничений SAT-решателями в процессе работы с трудными экземплярами задачи о булевой выполнимости. Данный феномен является следствием применения эвристических механизмов чистки конфликтных баз, которые реализованы во всех современных SAT-решателях, основанных на алгоритме CDCL (Conflict Driven Clause Learning). Описана новая техника, которая позволяет отслеживать повторно порождаемые дизъюнкты и запрещать их последующее удаление. На базе предложенных технических решений построен новый многопоточный SAT-решатель (SAT, SATisfiability), который на ряде SAT-задач, кодирующих обращение криптографических хеш-функций, существенно превзошел по эффективности многопоточные решатели, занимавшие в последние годы высокие места на специализированных соревнованиях.

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

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

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

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

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

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

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