Автор: Олег Сергеевич Заикин
Соавторы:
Заикин О.С.
Семенов А.А.
Посыпкин М.А.
Аннотация:
В статье предложен новый подход к построению декомпозиционных множеств, используемых для крупноблочного распараллеливания SAT-задач и их решения в распределенных вычислительных средах. Предложенные алгоритмы используется в проекте добровольных распределенных вычислений SAT@home.
Ключевые слова:
Выполнимость булевых формул, метод имитации отжига, добровольные распределенные вычисления, SAT@home.