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

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

Об'єктом задачі 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.