Вікіпедія

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

Інтерактивний перегляд історії
[неперевірена версія][неперевірена версія]
← Попереднє редагуванняНаступне редагування →
Вилучено вміст Додано вміст
ВізуальнийВікірозмітка
Addbot (обговорення | внесок)
Боти
140 524 редагування
м Вилучення 19 інтервікі, відтепер доступних на Вікіданих: d:q875276
шаблон
Рядок 6:
Згідно з [[Теорема Кука|теоремою Кука]], доведеною [[Кук, Стівен|Стівеном Куком]] в 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> символів, тобто довжина рядка зросте в [[многочлен|поліноміальне]] число разів.
Рядок 15:
Наприклад, формула <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]].
Рядок 34:
* [http://report.vtsnet.ru (питання зведення 3-SAT до 2-SAT)]
* [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-повні задачі]]}}▼
{{Без джерел|дата=жовтень 2008}}
{{math-stub}}
 
▲[[Категорія:NP-повні задачі]]
Отримано з https://uk.wikipedia.org/wiki/Задача_здійсненності_булевих_формул