W seminarium przedstawię dziewięć SAT-solverów, w tym nowoczesne narzędzia takie jak Lingeling, Glucose i Clasp, których efektywność zostanie porównana dla problemów obliczeniowych o różnej złożoności: od P (dwie popularne zagadki szachowe) do EXPTIME (wieże Hanoi), ale głównie będą to problemy NP-zupełne. Należą do nich problem odpowiedniości Posta (BPCP), extended string-to-string correction (ESCP) a także trzy klasyczne zagadnienia z teorii grafów. Ponadto dla niektórych problemów (m.in. BPCP i ESCP) definiujemy własne, oryginalne kodowania do SAT. Przedstawione wyniki eksperymentalne pozwalają na wyciągnięcie ciekawych wniosków odnośnie efektywności i przydatności SAT-solverów do rozwiązywania problemów o różnej złożoności. Ponadto, po przeprowadzonych testach analizuję formuły w postaci CNF zawarte w wygenerowanych benchmarkach w poszukiwaniu charakterystycznych wspólnych cech dla relatywnie najłatwiejszych i najtrudniejszych instancji.