Дубликаты конфликтных ограничений в CDCL-выводе и их использование в задачах обращения некоторых криптографических функций
Кондратьев В.С., Семенов А.А., Заикин О.С.

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

Ключевые слова: задача о булевой выполнимости (SAT), алгоритм CDCL, конфликтные дизъюнкты, криптографические хеш-функции.

Название статьи, аннотация и ключевые слова на английском языке

  • Кондратьев В.С. – Иркутский национальный исследовательский технический университет, ул. Лермонтова, 83, 664074, г. Иркутск; магистрант, e-mail: vikseko@gmail.com
  • Семенов А.А. – Институт динамики систем и теории управления имени В.М. Матросова СО РАН, ул. Лермонтова, 134, 664033, г. Иркутск; зав. лабораторией, e-mail: biclop.rambler@yandex.ru
  • Заикин О.С. – Институт динамики систем и теории управления имени В.М. Матросова СО РАН, ул. Лермонтова, 134, 664033, г. Иркутск; ст. науч. сотр., e-mail: zaikin.icc@gmail.com