Parallel algorithms for solving SAT-problems in application to optimization problems with Boolean constraints

Authors

  • O.S. Zaikin
  • I.V. Otpuschennikov
  • A.A. Semenov

Keywords:

inversion of discrete functions
satisfiability problem (SAT-problem)
Boolean equations
problems of combinatorial optimization

Abstract

A parallel technology that can be used to solve various problems of discrete optimization is proposed. This technology is based on a number of efficient procedures of reducing combinatorial optimization problems to SAT problems. A process of solving an optimization problem is implemented as an iterative scheme such that a SAT problem is solved at each step using various techniques of parallelization. In order to take into account the information accumulated during previous iterations, a special technique called «Incremental SAT» is used. This technique is usually applied to solve the verification problems for discrete systems. The technology proposed was tested using various combinatorial problems, in particular, the quadratic assignment problem.

New computational technologies

Downloads

Published

2011-04-11

Issue

Vol. 12 (2011): Issue 1.

Section

Section 1. Numerical methods and applications

Author Biographies

O.S. Zaikin

Matrosov Institute for System Dynamics and Control Theory of SB RAS (IDSTU SB RAS)
• Researcher

I.V. Otpuschennikov

Matrosov Institute for System Dynamics and Control Theory of SB RAS (IDSTU SB RAS)
• Programmer

A.A. Semenov

Matrosov Institute for System Dynamics and Control Theory of SB RAS (IDSTU SB RAS)
• Head of Laboratory

References

  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).