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

Авторы

  • О.С. Заикин
  • И.В. Отпущенников
  • А.А. Семенов

Ключевые слова:

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

Аннотация

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

Новые вычислительные технологии

Загрузки

Опубликован

2011-04-11

Выпуск

Том 12 (2011): Выпуск 1.

Раздел

Раздел 1. Вычислительные методы и приложения

Авторы

О.С. Заикин

Институт динамики систем и теории управления имени В.М. Матросова СО РАН (ИДСТУ СО РАН)
ул. Лермонтова, 134, 664033, Иркутск
• научный сотрудник

И.В. Отпущенников

Институт динамики систем и теории управления имени В.М. Матросова СО РАН (ИДСТУ СО РАН)
ул. Лермонтова, 134, 664033, Иркутск
• программист

А.А. Семенов

Институт динамики систем и теории управления имени В.М. Матросова СО РАН (ИДСТУ СО РАН)
ул. Лермонтова, 134, 664033, Иркутск
• заведующий лабораторией

Библиографические ссылки

  1. Rudeanu S. Boolean functions and equations. Amsterdam, London: North-Holland Publishing Company, 1974.
  2. Prestwich S. CNF encodings // Handbook of Satisfiability / Eds. A. Biere, M. Heule, H.van Maaren, T. Walsh. Amsterdam: IOS Press, 2009. 75-97.
  3. Cook S.A. The complexity of theorem-proving procedures // Proc. 3rd Ann. ACM Symp. on Theory of Computing (STOC 71). New York: ACM. 1971. 151-159.
  4. Garey M.R., Johnson S. Computers and intractability: A guide to the theory of NP-completeness. New York: W.H. Freeman, 1979.
  5. Семёнов А.А. Трансляция алгоритмов вычисления дискретных функций в выражения пропозициональной логики // Прикладные алгоритмы в дискретном анализе. Сер. Дискретный анализ и информатика. 2008. Вып. 2. Иркутск: Изд-во ИГУ. 70-98.
  6. Отпущенников И.В., Семенов А.А. Инструментальное средство трансляции алгоритмов вычисления дискретных функций в выражения исчисления высказываний. Свидетельство о государственной регистрации программы для ЭВМ N 2011611151 (03.02.2011).
  7. Заикин О.С., Семенов А.А. Технология крупноблочного параллелизма в SAT-задачах // Проблемы управления. 2008. N 1. 43-50.
  8. Заикин О.С. Реализация процедур прогнозирования трудоемкости параллельного решения SAT-задач // Вестник УГАТУ. 2010. 14, N 4(39). 210-220.
  9. AIG Format (http://fmv.jku.at/aiger/).
  10. Ахо А., Сети Р., Ульман Дж. Компиляторы. Принципы, технологии, инструменты. М., СПб, Киев: Вильямс, 2001.
  11. Menezes A., Oorschot P., Vanstone S. Handbook of applied cryptography. Boca Raton: CRC Press, 1996.
  12. Een N., Sorensson N. Translating pseudo-Boolean constraints into SAT // J. Satisfiability, Boolean Modeling and Computation. 2006. 2. 1-25.
  13. Espresso heuristic logic minimizer (http://embedded.eecs.berkeley.edu/pubs/downloads/espresso).
  14. Цейтин Г.С. О сложности вывода в исчислении высказываний // Записки научных семинаров ЛОМИ АН СССР. 1968. 8. 234-259.
  15. MiniSat+ solver (http://minisat.se/MiniSat.html).
  16. Beasley J.E. Or-library: distributing test problems by electronic mail // J. Oper. Res. Soc. 1990. 41, N 11. 1069-1072.
  17. CPLEX solver for linear and mixed integer programming (http://www.aimms.com/features/solvers/cplex).
  18. Cela E. The quadratic assignment problem: theory and algorithms. Berlin: Springer, 1998.
  19. QAPLIB - A Quadratic Assignment Problem Library (http://www.seas.upenn.edu/qaplib/).
  20. Minisat SAT Solver (http://www.minisat.se).
  21. Гришагин В.А., Свистунов А.Н. Параллельное программирование на основе MPI. Учебное пособие. Нижний Новгород: Изд-во ННГУ, 2005.
  22. Disch S., Scholl C. Combinational equivalence checking using incremental SAT solving, output ordering, and resets // ASP-DAC 2007. 938-943.
  23. MIPLIB - Mixed Integer Problem Library (http://miplib.zib.de).
  24. Суперкомпьютерный центр ИДСТУ СО РАН (http://www.mvs.icc.ru).