Реализация процедур прогнозирования трудоемкости параллельного решения SAT-задач

Abstract

Разработана и реализована в виде MPI-программы крупноблочная параллельная технология решения SAT-задач (задач поиска решений уравнений вида «КНФ = 1», где КНФ – конъюнктивная нормальная форма) в распределенных вычислительных средах. В рамках данной технологии осуществляется декомпозиция исходной SAT-задачи на семейство подзадач. Используется процедура статистического прогнозирования трудоемкости параллельного решения SAT-задач, которая позволяет определить оптимальные (по прогнозу) параметры декомпозиции. Использование параметров декомпозиции, найденных с помощью процедур прогнозирования, позволяет успешно решать SAT-задачи, кодирующие задачи обращения ряда криптографических дискретных функций.