Задача здійсненності булевих формул

Щоб чітко сформулювати задачу розпізнавання, необхідно домовитися про алфавіт, за допомогою якого задаються екземпляри мови. Цей алфавіт має бути фіксованим і скінченним. У своїй книзі Гопкрофт, Мотвані і Ульман пропонують використати наступний алфавіт: {"${\displaystyle \wedge }$", «${\displaystyle \vee }$», «${\displaystyle \neg }$», «${\displaystyle (}$», «${\displaystyle )}$», «${\displaystyle x}$», «${\displaystyle 0}$», «${\displaystyle 1}$»}.

При використанні такого алфавіту дужки і оператори записуються природним чином, а змінні отримують наступні імена: x1, x10, x11, x100 і т. д., згідно з їх номерами, записаними в двійковій системі числення.

Нехай деяка булева формула, записана в звичайній математичній нотації, мала б довжину ${\displaystyle N}$ символів. У ній кожне входження кожної змінної було описане хоча б одним символом, отже, всього в цій формулі не більше ${\displaystyle N}$ змінних. Значить, в запропонованій вище нотації кожна змінна буде записана за допомогою ${\displaystyle O\left(\log {N}\right)}$ символів. У такому разі, вся формула в новій нотації матиме довжину ${\displaystyle O\left(N\log {N}\right)}$ символів, тобто довжина рядка зросте в поліноміальне число разів.

Наприклад, формула ${\displaystyle a\wedge \neg (b\vee c)}$ набуде вигляду ${\displaystyle x1\wedge \neg (x10\vee x11)}$.

У 1971-му році в статті Стівена Кука був уперше введений термін «NP-повна задача», і задача SAT була першою задачею, для якого доводилася ця властивість.

У доказі теореми Кука кожна задача з класу NP в явному виді зводиться до SAT. Після появи результатів, Куком була доведена NP-повнота для безлічі інших задач. При цьому найчастіше для доказу NP-повноти деякої задачі наводиться поліноміальне зведення задачі SAT до цієї задачі, можливо в декілька кроків, тобто з використанням декількох проміжних задач.

Цікавими окремими випадками задачі SAT є:

• Задача здійсненності булевих формул в кон'юнктивній нормальній формі (SATCNF) — аналогічна задача, з накладеною на формулу умовою: вона має бути записана в кон'юнктивній нормальній формі.

• Задача здійсненності булевих формул в k-кон'юнктивній нормальній формі (k-SAT) — задача здійсненності за умови, що формула записана в k-кон'юнктивній нормальній формі. Ця задача є NP-повною при ${\displaystyle k\geq 3}$.

• Задача здійсненності булевих формул в 2-кон'юнктивній нормальній формі має поліноміальне рішення, тобто належить класу P.

• Satisfiability Modulo Theories
• Проблема трійок Буля — Піфагора

• (питання зведення 3-SAT до 2-SAT)^{[недоступне посилання з липня 2019]}
• The international SAT Competitions web page
• SATLIB — The Satisfiability Library
• Sat Live — загальний сайт про SAT.