Зада́ча здійсне́нності бу́левих фо́рмул (SAT, від англ. satisfiability) — важлива для теорії обчислювальної складності алгоритмічна задача.

Об'єктом задачі SAT є булева формула, що складається тільки з назв змінних, дужок і операцій ${\displaystyle \wedge }$ (І) ${\displaystyle \vee }$ (АБО) і ${\displaystyle \neg }$ (НІ). Задача полягає в наступному: чи можна призначити усім змінним, що трапляються у формулі, значення хибність і істина так, щоб формула стала істинною.

Згідно з теоремою Кука, доведеною Стівеном Куком в 1971-му році, задача SAT для булевих формул, записаних в кон'юнктивній нормальній формі, є NP-повною. Вимога про запис у кон'юнктивній формі є важливою, оскільки, наприклад, для формул, представлених в диз'юнктивній нормальній формі, задача SAT тривіально вирішується за лінійний час від розміру запису формули.

Щоб чітко сформулювати задачу розпізнавання, необхідно домовитися про алфавіт, за допомогою якого задаються екземпляри мови. Цей алфавіт має бути фіксованим і скінченним. У своїй книзі Гопкрофт, Мотвані і Ульман запропонували застосувати наступний алфавіт: {"${\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) [Архівовано 9 січня 2010 у Wayback Machine.]
• The international SAT Competitions web page [Архівовано 12 лютого 2005 у Wayback Machine.]
• SATLIB — The Satisfiability Library [Архівовано 11 лютого 2021 у Wayback Machine.]
• Sat Live [Архівовано 7 листопада 2020 у Wayback Machine.] — загальний сайт про SAT.

Ця стаття не містить посилань на джерела. Ви можете допомогти поліпшити цю статтю, додавши посилання на надійні (авторитетні) джерела. Матеріал без джерел може бути піддано сумніву та вилучено. (грудень 2015)

Ця стаття потребує додаткових посилань на джерела для поліпшення її перевірності. Будь ласка, допоможіть удосконалити цю статтю, додавши посилання на надійні (авторитетні) джерела. Зверніться на сторінку обговорення за поясненнями та допоможіть виправити недоліки. Матеріал без джерел може бути піддано сумніву та вилучено. (грудень 2015)

Це незавершена стаття з математики. Ви можете допомогти проєкту, виправивши або дописавши її.

Це незавершена стаття про алгоритми. Ви можете допомогти проєкту, виправивши або дописавши її.