Представления булевых функций: таблицы истинностей, деревья решений, КНФ, ДНФ, формулы в базисе AND-OR-NOT, ветвящиеся программы, булевы схемы.

Моделирование машин Тьюринга булевыми схемами. Класс NP, полные задачи. NP-полнота задачи SAT. Материалы: конспект курса Обзорный курс по теоретической информатике

Деревья решений, как доказательство невыполнимости формулы. Принцип Дирихле. Доказательство нижних оценок с помощью игры. Связь с методом резолюций. Материалы: конспект курса Сложность пропозициональных доказательств