A SERVICE FOR SOLVING BOOLEAN SATISFIABILITY PROBLEM USING NVIDIA CUDA TECHNOLOGY

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

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

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

The article presents a review of existing cat a real Mace task feasibility, the result of using the technology NVIDIA CUDA. Examines the main approaches to the parallelization of real rooms the method both full and local search. The description of these developed by the author of the article, the nano at the local search algorithm. The most current implementation, all with the help of the GPU. Also, given real numbers of local search method developed by the author. Open the tools developed using the tool HpcSoMasFramework. Using this service, provide a large number of experiments, the results of which were processed in automatic mode. The service showed its performance significantly and post the experiments. Given the chic algorithm, a plan for implementation. Way to open the scoring algorithm with the use of graphics URL. Describes one of the variants of the memory allocation between the Central and graphics processor. Give a description of the service to automate the solving of problems, the Mace feasibility and treatment results. This service provides access to Alan wise resource provides the interface plates for the formation of the task at the user's request, monitors execution of the job and notifies the user of the status of the request. Another way Funky designed service is the possibility of statistic processing of the obtained results and visualize the values of interest in a graph. In KL-Italy part of the article will be presented the experimental results obtained through the service Pan. The Dalai areas of research include the extension of functionalities of the service, and the development of additional tools for the solution of a discrete combination of tasks based on the SB-approach.

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

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, Vol. 35, pp. 19–151.

2. Oparin G.A., Bogdanova V.G. Instrumental'nye sredstva avtomatizatsii parallel'nogo resheniya bulevykh uravnenii na mno-goyadernykh protsessorakh [Automation tools for parallel solution of Boolean equations using multi-core processors]. Programmnye produkty i sistemy [Software & Systems], 2012, No. 1, pp. 10–14.

3. Bogdanova V.G., Gorskii S.A. Tekhnologiya parallel'nogo resheniya nelineinykh sistem bulevykh uravnenii na vychislitel'nom klastere [Technology of parallel solution of nonlinear systems of Boolean equations on a computing cluster]. Sovremennye tekhnologii. Sistemnyi analiz. Modelirovanie [Modern Technologies. System Analysis. Modeling], 2013, No. 1 (37), pp. 54–60.

4. Boreskov A.V., Kharlamov A.A. Osnovy raboty s tekhnologiei CUDA [Fundamentals of using the CUDA technology]. Moscow: DMKPress Publ., 2010, 232 p.

5. Bogdanova V.G., Gorskii S.A., Pashinin A.A. Servis-orientirovannye instrumental'nye sredstva dlya resheniya zadach bulevoi vypolnimosti [Service-oriented tools for solving Boolean satisfiability problems]. Fundamental'nye issledovaniya [Fundamental research], 2015, No. 2, Part 6, pp. 1151–1156.

6. Bychkov I.V. et al. Cervis-orientirovannyi podkhod k organizatsii raspredelennykh vychislenii s pomoshch'yu instrumental'nogo kompleksa DISCENT [A service-oriented approach to the organization of distributed computing using the DISCENT toolkit]. Informatsionnye tekhnologii i vychislitel'nye sistemy [Journal of Information Technologies and Computing Systems], 2014, No. 2, pp. 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, pp. 123–126.

8. Braunstein A., Mezard M., Zecchin R. Survey propagation: An algorithm for satisfiability. Random Structures and Algorithms, 2005, No. 27, pp. 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, pp. 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). Las Vegas, 2012, pp. 764–773.

11. Dal Palù, Dovier A., Formisano A., and Pontelli E. CUD@SAT: SAT Solving on GPUs. JETAI (Journal of Experimental & Theo-retical Artificial Intelligence), 2015, Vol. 27, Issue 3, pp. 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. URL: https://www.cs.rit.edu/. (access date: 05.08.2016).

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. Computation 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, pp. 27–31.

16. SATLIB - Benchmark Problems. URL:  http://www.cs.ubc.ca/~hoos/SATLIB/benchm. tml. (access date: 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.