SAT

SAT, от Satisfiability, в русскоязычной литературе — «Выполнимость». Формулировка задачи:

Дано булевское выражение, являющееся коньюнктивной нормальной формой (КНФ):

$\bigwedge_{i=1}^m K_i,$

где K_i — элементарные дизьюнкции вида

$x_{j_1}^{\sigma_1}\lor\ldots\lor x_{j_k}^{\sigma_k}$, $\sigma_j\in\{0,1\}$, $x^1=x$ и $x^0=(\neg x)$.

Существует ли (булевский) набор переменных x_j, обращающий эту форму в «1» (то есть в «TRUE»)?

Известно, что задача SAT — NP-полна.

Известные частные случаи — задачи 3SAT и 2SAT.

По крайней мере часть этого текста взята с ресурса http://lib.custis.ru/ под лицензией GDFL.Список авторов доступен на этом ресурсе в статье под тем же названием.