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

Матеріал з Вікіпедії — вільної енциклопедії.
Перейти до: навігація, пошук

Зада́ча здійсни́мості бу́льових фо́рмул (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.

Див. також[ред.ред. код]

Посилання[ред.ред. код]