Параллельные алгоритмы решения проблемы выполнимости в применении к оптимизационным задачам с булевыми ограничениями
Заикин О.С., Отпущенников И.В., Семенов А.А.

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

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

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

Заикин О.С., науч. сотр., e-mail: oleg.zaikin@icc.ru;   Отпущенников И.В., программист, e-mail: otilya@yandex.ru;   Семенов А.А., зав. лабораторией, e-mail: biclop@rambler.ru - Институт динамики систем и теории управления СО РАН, ул. Лермонтова, 134, 664033, г. Иркутск