Параллельные алгоритмы решения проблемы выполнимости в применении к оптимизационным задачам с булевыми ограничениями

Предложена параллельная технология, которая может использоваться при решении ряда задач дискретной оптимизации. Технология основана на эффективных процедурах сведения задач комбинаторной оптимизации к задачам выполнимости (SAT-задачам). Процесс решения оптимизационной задачи реализован в виде итерационной схемы, каждый этап которой - это решение некоторой SAT-задачи. Получаемые SAT-задачи решаются при помощи различных схем распараллеливания. Для учета информации, накопленной в предыдущих итерациях, реализована техника “Incremental SAT”, применяемая в задачах верификации моделей дискретных систем. Разработанная технология была протестирована на некоторых комбинаторных задачах, в частности на квадратичной задаче о назначениях. Работа выполнена при поддержке гранта “Лаврентьевский конкурс молодежных проектов СО РАН” на 2010-2011 гг. и при финансовой поддержке РФФИ (код проекта 11-07-00377-а). Статья рекомендована к публикации Программным комитетом Международной научной конференции “Параллельные вычислительные технологии” (ПАВТ-2011; http://agora.guru.ru/pavt2011).