Задача о выполнимости булевых формул заключается в проверке выполнимости формулы логики высказываний. Требуется найти интерпретацию, в которой формула истинна, т.е. ищется такое присваивание истинностных значений (true или false) атомарным формулам в исходной формуле, при которых исходная формула станет истинной. В общем случае задача является NP-полной. Обычно исходная булева формула представляется в КНФ, т.е. в виде конъюнкции дизъюнктов (дизъюнкций). При этом задачу называют задачей о k-выполнимости, если максимальное число литералов в дизъюнкте (длина дизъюнкта) равно k. Если k2, то задача имеет полиномиальную сложность, иначе задача NP-полная.