Зада́ча здійсне́нності бу́левих фо́рмул (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.
Див. також
- (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.
Ця стаття не містить . (грудень 2015) |
Ця стаття потребує додаткових для поліпшення її . (грудень 2015) |
![]() | Це незавершена стаття з математики. Ви можете проєкту, виправивши або дописавши її. |
![]() | Це незавершена стаття про алгоритми. Ви можете проєкту, виправивши або дописавши її. |
Вікіпедія, Українська, Україна, книга, книги, бібліотека, стаття, читати, завантажити, безкоштовно, безкоштовно завантажити, mp3, відео, mp4, 3gp, jpg, jpeg, gif, png, малюнок, музика, пісня, фільм, книга, гра, ігри, мобільний, телефон, android, ios, apple, мобільний телефон, samsung, iphone, xiomi, xiaomi, redmi, honor, oppo, nokia, sonya, mi, ПК, web, Інтернет