Object

Abstrakt:

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

Data wydania:

2014-12-05

Identyfikator:

oai:ribes-88.man.poznan.pl:1561 ; doi:10.37055/sbn/135242 ; oai:editorialsystem.com:article-135242

ISSN drukowany:

2082-2677

Identyfikator wydawcy:

135242

Licencja:

click here to follow the link

Strona początkowa:

341

Strona końcowa:

357

Tom:

6

Wydanie:

2

Czasopismo:

SBN

Słowa kluczowe:

spełnialność formuł logicznych ; SAT Solver ; WalkSAT ; karty graficzne ; kryptoanaliza ; OpenCL ; obliczenia równoległe