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

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

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

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

Точне формулювання

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

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

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

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

Обчислювальна складність

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

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

Окремі випадки задачі SAT

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

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

• Задача здійсненності булевих формул у k-кон'юнктивній нормальній формі (k-SAT) — задача здійсненності за умови, що формула записана в k-кон'юнктивній нормальній формі. Ця задача є NP-повною при $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.