Цель курса – сформировать представление о важности задачи SAT, о теоретической основе данной задачи и об основных методах решения данной задачи. Дать представление о применимости методов решения задачи SAT в различных сферах математики и информатики, особенно в сфере автоматизированного доказательства теорем. Познакомить со способами реализации методов решения задачи SAT в программных системах для автоматической проверки выполнимости булевых формул.