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

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

Об'єктом задачі '''SAT''' є [[булева формула]], що складається тільки з імен змінних, дужок і операцій <math>\wedge</math> (''І'') <math>\vee</math> (''АБО'') і <math>\neg</math> (''НІ'').
Задача полягає в наступному: чи можна призначити усім змінним, що зустрічаються у формулі, значення ''хибність'' і ''істина'' так, щоб формула стала істинною.

Згідно з [[Теорема Кука — Левіна|теоремою Кука]], доведеною [[Стівен Кук|Стівеном Куком]] в 1971-му році, задача SAT для булевих формул, записаних в [[Кон'юнктивна нормальна форма|кон'юнктивній нормальній формі]], є [[NP-повна задача|NP-повною]]. Вимога про запис в кон'юнктивній формі є важливою, оскільки, наприклад, завдання SAT для формул, представлених в [[Диз'юнктивна нормальна форма|диз'юнктивній нормальній формі]], тривіально вирішується за лінійний час залежно від розміру запису формули.

== Точне формулювання ==
Щоб чітко сформулювати [[задача розпізнавання|задачу розпізнавання]], необхідно домовитися про алфавіт, за допомогою якого задаються екземпляри мови. Цей алфавіт має бути фіксованим і скінченним. <!-- виправити!!! -->У своїй книзі [[Джон Гопкрофт|Гопкрофт]], Мотвані і Ульман пропонують використати наступний алфавіт: {"<math>\wedge</math>", «<math>\vee</math>», «<math>\neg</math>», «<math>(</math>», «<math>)</math>», «<math>x</math>», «<math>0</math>», «<math>1</math>»}.

При використанні такого алфавіту дужки і оператори записуються природним чином, а змінні отримують наступні імена: x1, x10, x11, x100 і&nbsp;т.&nbsp;д., згідно з їх номерами, записаними в [[двійкова система числення|двійковій системі числення]].

Нехай деяка [[булева формула]], записана в звичайній математичній нотації, мала б довжину <math>N</math> символів. У ній кожне входження кожної змінної було описане хоча б одним символом, отже, всього в цій формулі не більше <math>N</math> змінних. Значить, в запропонованій вище нотації кожна змінна буде записана за допомогою <math>O\left(\log{N}\right)</math> символів. У такому разі, вся формула в новій нотації матиме довжину <math>O\left(N\log{N}\right)</math> символів, тобто довжина рядка зросте в [[многочлен|поліноміальне]] число разів.

Наприклад, формула <math>a\wedge\neg(b\vee c)</math> набуде вигляду <math>x1\wedge\neg(x10\vee x11)</math>.

== Обчислювальна складність ==
У 1971-му році в статті [[Стівен Кук|Стівена Кука]] був уперше введений термін «[[NP-повна задача]]», і задача SAT була першою задачею, для якого доводилася ця властивість.

У доказі [[Теорема Кука — Левіна|теореми Кука]] кожна задача з [[Клас складності NP|класу NP]] в явному виді зводиться до SAT. Після появи результатів, Куком була доведена NP-повнота для безлічі інших задач. При цьому найчастіше для доказу NP-повноти деякої задачі наводиться [[поліноміальне зведення]] задачі SAT до цієї задачі, можливо в декілька кроків, тобто з використанням декількох проміжних задач.

== Окремі випадки задачі SAT ==
Цікавими окремими випадками задачі SAT є:
* Задача здійсненності булевих формул в кон'юнктивній нормальній формі (SATCNF)&nbsp;— аналогічна задача, з накладеною на формулу умовою: вона має бути записана в [[кон'юнктивна нормальна форма|кон'юнктивній нормальній формі]].

* Задача здійсненності булевих формул в k-кон'юнктивній нормальній формі (k-SAT)&nbsp;— задача здійсненності за умови, що формула записана в k-кон'юнктивній нормальній формі. Ця задача є [[NP-повна задача|NP-повною]] при <math>k\geq 3</math>.

* Задача здійсненності булевих формул в 2-кон'юнктивній нормальній формі має поліноміальне рішення, тобто належить [[Клас складності P|класу P]].

== Див. також ==
* [[Satisfiability Modulo Theories]]
* [[Проблема трійок Буля — Піфагора]]

== Посилання ==
* [http://report.vtsnet.ru (питання зведення 3-SAT до 2-SAT)]{{Недоступне посилання|date=липень 2019 |bot=InternetArchiveBot }}
* [http://www.satcompetition.org/ The international SAT Competitions web page]
* [http://www.satlib.org/ SATLIB&nbsp;— The Satisfiability Library]
* [http://www.satlive.org/ Sat Live]&nbsp;— загальний сайт про SAT.

{{NP-повні задачі}}
{{Логіка}}
{{math-stub}}
{{Algorithm-stub}}
{{Без джерел|дата=грудень 2015}}
{{Refimprove|дата=грудень 2015}}
[[Категорія:Логіка в інформатиці]]