A SAT-probléma vizsgálatához kapcsolódó kutatások, annak eldöntésére törekszenek, hogy egy formula  konjunktív normálforma alakjáról minnél kevesebb idő allatt eldöntsék, hogy kielégíthető-e.  Ha a formula n atomból (logikai változóból) áll,  akkor legrosszabb esetben 2^n próbálkozásból megállapítható, hogy
kielégíthető-e a formula. A SAT probléma jól ismert NP-teljes probléma.  Cikkünkben megvizsgálunk és összehasonlítunk különböző párhuzamosított és  szekvenciális SAT megoldó alkalmazásokat. A vizsgálatainkat elsősorban arra  fókuszáljuk, hogy elosztott környezetben milyen megoldások léteznek a kommunikáció okozta sebességcsökkenés kiküszöbölésére, illetve milyen  stratégiákat használnak az algoritmus párhuzamosítására. Elemezzük az  egyes rendszerek hibatűrő képességét, illetve vizsgáljuk, hogy mennyire  megoldott a hibakeresés.