Celem przedmiotu jest zaznajomienie słuchaczy z podstawowymi zagadnieniami teorii obliczeń oraz omówienie praktycznych zastosowań tej teorii, ze szczególnym uwzględnieniem implementowania algorytmów korzystających z narzędzi takich, jak SAT solvery, SMT solvery czy QBF solvery.
Program przedmiotu obejmuje: modele obliczeń (automaty i maszyny), praktyczne klasy złożoności obliczeniowej (LogSpace, P, NP, PSpace), dyskusję o problemach nienależących do tych klas oraz omówienie narzędzi i technik wykorzystywanych do radzenia sobie z problemami o dużej złożoności.
Przedmiot ten nie będzie trudny: powinien być przystępny dla studentów trzeciego semestru. Zajęcia pomocnicze będą składały się z list zadań rozwiązywanych w trakcie zajęć oraz z zadań domowych (implementacyjnych oraz teoretycznych).
