Задача выполнимости булевых формул (SAT) состоит в том, чтобы определить, существует ли способ присвоить переменным значения «истина» или «ложь» так, чтобы заданная булева формула приняла значение «истина». Несмотря на простоту постановки, SAT является одной из центральных задач теории вычислительной сложности, а также активно применяется на практике: многие вычислительные и комбинаторные задачи можно представить в виде булевых формул, а затем решать с помощью современных SAT-солверов.
Помимо классической постановки существует множество вариаций этой задачи. В них может требоваться, например, максимизировать число выполненных клозов, найти решение с заданными свойствами или определить выполнимость формулы определенного вида. В рамках данного направления мы исследуем вычислительную сложность этих задач и её зависимость от естественных параметров, таких как длина формулы, число переменных, необходимое количество выполненных клозов и т. д. Особое внимание уделяется разработке и теоретическому анализу алгоритмов, а также выявлению структурных свойств формул, оказывающих существенное влияние на вычислительную сложность задачи.