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

Зада́ча здійсни́мості бу́льових фо́рмул (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)
• The international SAT Competitions web page
• SATLIB - The Satisfiability Library
• Sat Live - загальний сайт про SAT.