СЕРВИС ДЛЯ РЕШЕНИЯ ЗАДАЧ БУЛЕВОЙ ВЫПОЛНИМОСТИ С ПРИМЕНЕНИЕМ ТЕХНОЛОГИИ NVIDIA CUDA

Дата поступления: 
11.12.2017
Год: 
2017
Номер журнала (Том): 
УДК: 
004.421
DOI: 

10.26731/1813-9108.2017.4(56).107-114

Файл статьи: 
Страницы: 
107
114
Аннотация: 

В статье представлен краткий обзор существующих решателей задач булевой выполнимости, ускоренных с применением технологии NVIDIA CUDA. Рассматриваются основные подходы к распараллеливанию решателей, основанных на методах как полного, так и локального поиска. Представлено описание решателя, разработанного автором статьи, основанного на алгоритме локального поиска. Рассмотрены наиболее заметные реализации решателей, распараллеленных при помощи GPU. Также приведён решатель, основанный на методе локального поиска, разработанный автором. Описан сервис, разработанный с использованием инструментария HpcSoMas Framework. С помощью данного сервиса проведено большое количество экспериментов, результаты которых были обработаны в автоматическом режиме. Сервис показал свою работоспособность и значительно упростил проведение экспериментов. Приведён пошаговый алгоритм, использованный для реализации. Описан способ ускорения алгоритма с применением графического ускорителя. Рассматривается один из вариантов распределения памяти между центральным и графическим процессором. Приведено описание сервиса для автоматизации решения задач булевой выполнимости и обработки результатов. Данный сервис обеспечивает удаленный доступ к вычислительному ресурсу, предоставляет пользовательский интерфейс для формирования задания по запросу пользователя, осуществляет мониторинг выполнения задания и уведомляет пользователя о статусе запроса. Другой важной функцией разработанного сервиса является возможность статистической обработки полученных результатов и визуализации  интересующих значений в виде графиков. В заключительной части статьи представлены результаты вычислительных экспериментов, полученные с помощью описанного сервиса. К дальнейшим направлениям исследования можно отнести расширение функциональных возможностей сервиса, а также разработку дополнительных инструментальных средств для решения дискретных комбинаторных задач на основе SAT-подхода.

Список цитируемой литературы: 

1. Gu J., Purdom P.W., Franco J., and Wah B. Algorithms for the Satisfability problem: a survey // DIMACS Series on Discrete Mathematics and Theoretical Computer Science, American  Mathematical  Society. – 1997. –  V. 35. – P.19-151.

2. Опарин Г.А., Богданова В.Г. Инструменталь-ные средства автоматизации параллельного решения булевых уравнений на многоядер-ных процессорах // Программные продукты и системы. – 2012. – № 1. – С. 10-14.

3. Богданова В.Г., Горский С.А. Технология параллельного решения нелинейных систем булевых уравнений на вычислительном кла-стере // Современные технологии. Системный анализ. Моделирование. – 2013. – № 1 (37). –  С. 54-60.

4. Боресков А.В., ХарламовА.А. Основы рабо-ты с технологией CUDA // М.:ДМКПресс, 2010. — 232 с. ISBN 978-5-94074-578-5.

5. Богданова В.Г., Горский С.А., Пашинин А.А. Сервис-ориентированные инструментальные средства для решения задач булевой выполнимости // Фундаментальные исследования. – 2015. – № 2 (часть 6). – С.1151-1156.

6. Бычков И.В., Опарин Г.А., Феоктистов А.Г., Богданова В.Г., Корсуков А.С. Cервис-ориентированный подход к организации рас-пределенных вычислений с помощью инструментального комплекса DISCENT // Информационные технологии и вычислительные системы. – 2014. – № 2. – С. 7-15.

7. Gulati K., Khatri S. P. Boolean Satisfiability on a Graphics Processor // In Proceedings of the 20th Great Lakes Symposium on VLSI (GLSVLSI’10). – 2010. – P. 123–126.

8. Braunstein A., Mezard M., Zecchin R. Survey propagation: An algorithm for satisfiability // Random Structures and Algorithms. –  2005 (27) . – P.201–226.

9. Meyer Q., Schonfeld F., Stamminger M. et al. 3-SAT on CUDA: Towards a Massively Parallel SAT Solver // High Performance Computing and Simulation (HPCS). –  2010. – P. 306-313.

10. Hironori F., Noriyuki F. GPU Acceleration of BCP Procedure for SAT Algorithms // The 2012 International Conference on Parallel and Distributed Processing Techniques and Applications (PDPTA’12). 16 July 2012. – Las Vegas, 2012. – P. 764-773.

11. Dal Palù, Dovier A., Formisano A., and Pon-telli E. CUD@SAT: SAT Solving on GPUs // JETAI (Journal of Experimental & Theoretical Artificial Intelligence). – 2015. – V.27. – Issue 3. – P. 293-316.

12. Costa C.S. Parallelization of SAT Algorithms on GPUs. Technical report, INESC-ID, Technical University of Lisbon. – 2013.

13. Wang Y. NVIDIA CUDA Architecture-based Parallel Incomplete SAT Solver - 2010 - cs.rit.edu.

14. Kolomycki M. Use NVIDIA CUDA technology to create genetic algorithms with extensive population - 2013 - hgpu.org

15. Z. Luo. G.A., Z. Yang, H. Liu et al. Computa-tion of 3-SAT problem on Graphic Process Unit // Proceedings of the International Symposium on Intelligent Computation and its Application. – Wuhan: China University of Geosciences Press, 2005. – P. 27-31.

16. http://www.cs.ubc.ca/~hoos/SATLIB/benchm. tml. (дата обращения: 05.08.2016).

17. Елисеев С.В., Банина Н.В., Ахмадеева А.А., Гозбенко В.Е. Математические модели и анализ динамических свойств механических систем // депонированная рукопись  № 782-В2009 08.12.2009.

18. Хоменко А.П., Елисеев С.В., Гозбенко В.Е., Банина Н.В. Устройство для управления со-стоянием объекта защиты // патент на полез-ную модель RUS 56858 21.04.2006.

19. Гозбенко В.Е., Карлина А.И., Каргапольцев С.К. Главные координаты в решении задач вертикальной динамики транспортного средства // Системы. Методы. Технологии. 2016. № 3 (31). С. 58-62.

20. Gozbenko V.E., Kargapoltsev S.K., Kornilov D.N., Minaev N.V., Karlina A.I. Definition of the main coordinates of the car with two-level spring suspension // International Journal of Applied Engineering Research. 2016. Т. 11. № 20. С. 10367-10373.

21. Карлина А.И., Каргапольцев С.К., Гозбенко В.Е. Приведение обобщенных сил в математических моделях транспортных систем // Современные технологии. Системный анализ. Моделирование. 2016. № 3 (51). С. 175-179.

22. Гозбенко В.Е., Каргапольцев С.К., Карлина А.И. Приведение динамической системы с тремя степенями свободы к главным координатам // Современные технологии. Системный анализ. Моделирование. 2016. № 3 (51). С. 35-38.

23. Карлина А.И., Гозбенко В.Е. Моделиро-вание объектов машиностроения для снижения влияния внешних вибрационных воздействий // Вестник Иркутского государственного технического уни-верситета. 2016. Т. 20. № 10. С. 35-47.

24. Gozbenko V.E., Kargapoltsev S.K., Minaev N.V., Karlina A.I. Simulation of the vibration of the carriage asymmetric parameters in mathcad // International Journal of Applied Engineering Research. 2016. Т. 11. № 23. С. 11132-11136.

25. Gozbenko V.E., Kargapolcev S.K., Kondratiev V.V., Minaev N.V., Karlina A.I. Vertical dynamics of the vehicle taking into account roughness gauge // Fundamental and Applied Studies in the Modern World Papers and Commentaries. Editor-in-Chief: Prof. Richard Dixon, D. Litt. et Phil. (UK), Publication Director: Prof. Kevin Barrington, D. S. Sc. (UK), Technical Editors: Molly Carpenter, Jeff Goodwin (UK) . 2016. С. 373-383.

26. Гозбенко В.Е., Карлина А.И. Математическая модель вагона с двумя степенями свободы, находящегося под действием периодической вынуждающей силы // Известия Транссиба. 2016. № 3 (27). С. 23-31.