Задача здійсненності булевих формул
Зада́ча здійсне́нності бу́левих фо́рмул (SAT, від англ. satisfiability) — важлива для теорії обчислювальної складності алгоритмічна задача.
Об'єктом задачі SAT є булева формула, що складається тільки з назв змінних, дужок і операцій (І) (АБО) і (НІ). Задача полягає в наступному: чи можна призначити усім змінним, що трапляються у формулі, значення хибність і істина так, щоб формула стала істинною.
Згідно з теоремою Кука, доведеною Стівеном Куком в 1971-му році, задача SAT для булевих формул, записаних в кон'юнктивній нормальній формі, є NP-повною. Вимога про запис у кон'юнктивній формі є важливою, оскільки, наприклад, для формул, представлених в диз'юнктивній нормальній формі, задача SAT тривіально вирішується за лінійний час від розміру запису формули.
Точне формулювання[ред. | ред. код]
Щоб чітко сформулювати задачу розпізнавання, необхідно домовитися про алфавіт, за допомогою якого задаються екземпляри мови. Цей алфавіт має бути фіксованим і скінченним. У своїй книзі Гопкрофт, Мотвані і Ульман запропонували застосувати наступний алфавіт: {"", «», «», «», «», «», «», «»}.
При застосуванні такого алфавіту дужки й оператори записуються природним чином, а змінні отримують такі назви: x1, x10, x11, x100 і т. д., згідно з їх номерами, записаними в двійковій системі числення.
Нехай деяка булева формула, записана в звичайній математичній нотації, має довжину символів. У ній кожне входження кожної змінної описано хоча б одним символом, отже, всього в цій формулі не більше змінних. Значить, у запропонованій вище нотації кожна змінна буде записана за допомогою символів. У такому разі, вся формула в новій нотації матиме довжину символів, тобто довжина рядка зросте в поліноміальну кількість разів.
Наприклад, формула набуде вигляду .
Обчислювальна складність[ред. | ред. код]
У 1971-му році в статті Стівена Кука був уперше введений термін «NP-повна задача», і задача SAT була першою задачею, для якої доводилася ця властивість.
У доказі теореми Кука кожна задача з класу NP в явному виді зводиться до SAT. Після появи результатів, Кук довів NP-повноту для багатьох інших задач. При цьому найчастіше для доказу NP-повноти деякої задачі наводиться поліноміальне зведення задачі SAT до цієї задачі, можливо, в декілька кроків, тобто, з використанням кількох проміжних задач.
Окремі випадки задачі SAT[ред. | ред. код]
Цікавими окремими випадками задачі SAT є:
- Задача здійсненності булевих формул у кон'юнктивній нормальній формі (SATCNF) — аналогічна задача, з накладеною на формулу умовою: вона має бути записана в кон'юнктивній нормальній формі.
- Задача здійсненності булевих формул у k-кон'юнктивній нормальній формі (k-SAT) — задача здійсненності за умови, що формула записана в k-кон'юнктивній нормальній формі. Ця задача є NP-повною при .
- Задача здійсненності булевих формул у 2-кон'юнктивній нормальній формі має поліноміальний розв'язок, тобто належить класу P.
Див. також[ред. | ред. код]
Посилання[ред. | ред. код]
- (питання зведення 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) |
Це незавершена стаття з математики. Ви можете допомогти проєкту, виправивши або дописавши її. |
Це незавершена стаття про алгоритми. Ви можете допомогти проєкту, виправивши або дописавши її. |
|
|