ПАРАЛЛЕЛЬНАЯ ПРОВЕРКА ДНФ НА ТАВТОЛОГИЮ

Рассматривается одна из базовых задач логико-комбинаторных вычислений – проверка дизъюнктивной нормальной формы на тавтологию. Предлагаются два алгоритма параллельного решения этой задачи с использованием многопроцессорных систем. Приводятся результаты экспериментальных испытаний предложенных алгоритмов на суперкомпьютере семейства СКИФ, показывающие эффективность параллельных вычислений при решении логико-комбинаторной задачи.