Rozwiązanie problemu trójspełnialności formuł logicznych z użyciem architektury CUDA

Widuch, J.; Krawczyk, K.

Artykuł - szczegóły

Tytuł artykułu

Rozwiązanie problemu trójspełnialności formuł logicznych z użyciem architektury CUDA

Autorzy

Widuch J. , Krawczyk K.

Identyfikatory

Warianty tytułu

Solving the 3-satisfiability problem using CUDA architecture

Języki publikacji

Abstrakty

Architektura CUDA firmy NVIDIA jest architekturą wielordzeniowych procesorów graficznych, w której jest stosowany model przetwarzania wielowątkowego. Procesor graficzny w architekturze CUDA może być traktowany jako procesor SIMD z pamięcią wspólną. W niniejszym artykule przedstawiono zastosowanie CUDA do rozwiązania problemu 3–SAT. Przedstawione zostały 3 wersje algorytmu oraz wyniki przeprowadzonych badań eksperymentalnych.

The NVIDIA's CUDA architecture is multi–core GPU architecture with the multithreaded processing model. The GPU of CUDA architecture can be treated as a SIMD processor with shared memory. This work presents solving the 3–SAT problem using CUDA architecture. Three versions of algorithm are proposed. Apart from that the results of experimental tests are presented.

Słowa kluczowe

GPGPU CUDA wielowątkowość SIMD problem 3-SAT

GPGPU CUDA multithreading SIMD 3-SAT problem

Wydawca

Wydawnictwo Politechniki Śląskiej

Czasopismo

Studia Informatica

Rocznik

2013

Tom

Vol. 34, nr 4

Strony

23--43

Opis fizyczny

Bibliogr. 25 poz.

Twórcy

autor

Widuch J.

jacek.widuch@polsl.pl

Politechnika Śląska, Instytut Informatyki Gliwice, Akademicka 16

autor

Krawczyk K.

rafalkrawczyk88@gmail.com

Bibliografia

1. Balint A., Fröhlich A.: Improving Stochastic Local Search for SAT with a New Probability Distribution. LNCS, Vol. 6175, Springer, Heidelberg 2010, p. 10-15.
2. Belov A., Järvisalo M., Stachniak Z.: Depth-Driven Circuit-Level Stochastic Local Search for SAT. Proceedings of the 22nd International Joint Conference on Artificial Intelligence (IJCAI, 2011), Barcelona, Spain 2011, p. 504-509.
3. Ben-Ari M.: Logika matematyczna w informatyce. WNT, Warszawa 2006.
4. Bhalla A., Lynce I., Sousa J. Marques-Silva J.: Heuristic Backtracking Algorithms for SAT. [In:] International Workshop on Microprocessor Test and Verification, Austin, Texas, USA, IEEE Computer Society, 2003, p. 69-74.
5. Cormen T. H., Leiserson C. E., Rivest R. L.: Wprowadzenie do algorytmów. WNT, Warszawa 2000.
6. Czech Z.: Wprowadzenie do obliczeń równoległych. Wydawnictwo Naukowe PWN, Warszawa 2010.
7. Davis M., Logemann G., Loveland D.: A machinę program for theorem proving. Communactions of the ACM, Vol. 5(7), 1962, p. 394-397.
8. Davis M., Putnam H.: A computing procedurę for ąuantification theory. Journal of the ACM, Vol. 7(3), 1960, p. 201-215.
9. Deleau H., Jaillet C, Krajecki M.: GPU4SAT: solving the SAT problem on GPU. In PARA 2008 9th International Workshop on State-of-the-Art in Scientific and Parallel Computing, Trondheim, Norway 2008.
10. Eén N., Sörensson N.: An extensible SAT-solver. In: Giunchiglia E., Tacchella A. (eds.) SAT 2003. LNCS, Vol. 2919, Springer, Heidelberg 2004, p. 502-518.
11. Galio G., Urbani G.: Algorithms for Testing the Satisfiability of Propositional Formulae. Journal of Logic Programming, Vol. 7, 1989, p. 45-61.
12. Haskins J.: 3SAT Solver, http://www.cs.virginia.edu/~jwh6q/3sat-web/.
13. Kirk D. B., Hwu W. W.: Programming Massively Parallel Processors: A Hands-on Approach. Morgan Kaufmann, lst edition (February 5, 2010).
14. Luba T., Rawski M., Tomaszewicz P., Zbierzchowski B.: Synteza układów cyfrowych. WKŁ, Warszawa 2003.
15. Mahajan Y. S., Fu Z., Malik S.: Zchaff2004: An efficient SAT solver. [In:] Hoos H.H., Mitchell D. G. (eds.): SAT 2004, LNCS 3542, Springer, Heidelberg 2005.
16. Marques-Silva J. P., Sakallah K. A.: GRASP: A search algorithm for propositional satisfiability. IEEE Transactions on Computers, Vol. 48, No. 5, 1999, p. 506-521.
17. Meyer Q., Schönfeld F., Stamminger M., Wańka R.: 3-SAT on CUDA: Towards amassively parallel SAT solver. Proceedings of High Performance Computing and Simulation (HPCS), 2010, p. 306-313.
18. Papadimitriou Ch.: Złożoność obliczeniowa. Helion, Gliwice 2012.
19. Rauber T., Riinger G.: Parallel Programming for Multicore and Cluster Systems. Springer, lst edition (March 10, 2010).
20. Sanders J., Kandrot E.: CUDA by Example: An Introduction to General-Purpose GPU Programming. Addison-Wesley Professional, lst edition (July 30, 2010).
21. Zabih R., McAllester D.: A Rearrangement Search Strategy for Determining Propositional Satisfiability. Proceedings of the National Conference on Artificial Intelligence, 1988, p. 155-160.
22. CUDA C Best Practices Guide Version 5.0. NVIDIA Corporation (October, 2012), https://developer.nvidia.com/cuda-downloads.
23. CUDA C Programming Guide Version 5.0. NVIDIA Corporation (October, 2012), https://developer.nvidia.com/cuda-downloads.
24. CUDA Reference Manuals Version 5.0. NVIDIA Corporation (October, 2012), https://developer.nvidia.com/cuda-downloads.
25. GeForce GTX 650 specifications, http://www.geforce.com/hardware/desktop-gpus/geforce-gtx-650/specifications.

Typ dokumentu

Bibliografia

Identyfikator YADDA

bwmeta1.element.baztech-dc557cdc-6460-4ebf-b0fd-265178f54c12