|
Вычислительные методы и программирование, 2019, том 20, выпуск 1, страницы 54–66
(Mi vmp947)
|
|
|
|
Дубликаты конфликтных ограничений в CDCL-выводе и их использование в задачах обращения некоторых криптографических функций
В. С. Кондратьевa, А. А. Семеновb, О. С. Заикинb a Национальный исследовательский Иркутский государственный технический университет
b Институт динамики систем и теории управления имени В.М. Матросова Сибирского отделения Российской академии наук, г. Иркутск
Аннотация:
Изучен феномен повторного порождения конфликтных ограничений SAT-решателями в процессе работы с трудными экземплярами задачи о булевой выполнимости. Данный феномен является следствием применения эвристических механизмов чистки конфликтных баз, которые реализованы во всех современных SAT-решателях, основанных на алгоритме CDCL (Conflict Driven Clause Learning). Описана новая техника, которая позволяет отслеживать повторно порождаемые дизъюнкты и запрещать их последующее удаление. На базе предложенных технических решений построен новый многопоточный SAT-решатель (SAT, SATisfiability), который на ряде SAT-задач, кодирующих обращение криптографических хеш-функций, существенно превзошел по эффективности многопоточные решатели, занимавшие в последние годы высокие места на специализированных соревнованиях.
Ключевые слова:
задача о булевой выполнимости (SAT), алгоритм CDCL, конфликтные дизъюнкты, криптографические хеш-функции.
Поступила в редакцию: 14.01.2019
Образец цитирования:
В. С. Кондратьев, А. А. Семенов, О. С. Заикин, “Дубликаты конфликтных ограничений в CDCL-выводе и их использование в задачах обращения некоторых криптографических функций”, Выч. мет. программирование, 20:1 (2019), 54–66
Образцы ссылок на эту страницу:
https://www.mathnet.ru/rus/vmp947 https://www.mathnet.ru/rus/vmp/v20/i1/p54
|
Статистика просмотров: |
Страница аннотации: | 165 | PDF полного текста: | 105 |
|