Problem spełnialności formuł rachunku zdań SAT jest jednym z fundamentalnych oraz otwartych zadań we współczesnej informatyce. Jest on problemem N P-zupełnym. To znaczy, że wszystkie problemy z klasy NP możemy sprowadzić do problemu SAT w czasie wielomianowym. Co ciekawe, wśród problemów z klasy NP istnieje wiele takich, które są ściśle związanych z kryptologią, na przykład: faktoryzacja liczb – ważna dla RSA, łamanie kluczy szyfrów symetrycznych, znajdowanie kolizji funkcji skrótu i wiele innych. Odkrycie wielomianowego algorytmu dla SAT skutkowa- łoby rozwiązaniem problemu milenijnego: P vs. NP. Cel ten wydaje się bardzo trudny do osiągnięcia – nie wiadomo nawet czy jest możliwy. Mając nieco mniejsze aspiracje możemy projektować algorytmy heurystyczne lub losowe dla SAT. W związku z tym, głównym celem autorów pracy jest przedstawienie projektu równoległego SAT Solvera bazującego na algorytmie WalkSAT, w tym procesu jego implementacji z wykorzystaniem środowiska programistycznego OpenCL oraz komputera wyposażonego w karty graficzne NVIDIA Tesla. Wraz z dynamicznym rozwojem technologii procesorów typu GPU oraz układów FPGA, jak również przenośnością rozwiązań stworzonych w OpenCL, kierunek takich prac staje się interesujący ze względu na uzyskiwaną efektywność obliczeniową, jak również szybkość prototypowania rozwiązań.