Для установки нажмите кнопочку Установить расширение. И это всё.

Исходный код расширения WIKI 2 регулярно проверяется специалистами Mozilla Foundation, Google и Apple. Вы также можете это сделать в любой момент.

4,5
Келли Слэйтон
Мои поздравления с отличным проектом... что за великолепная идея!
Александр Григорьевский
Я использую WIKI 2 каждый день
и почти забыл как выглядит оригинальная Википедия.
Статистика
На русском, статей
Улучшено за 24 ч.
Добавлено за 24 ч.
Что мы делаем. Каждая страница проходит через несколько сотен совершенствующих техник. Совершенно та же Википедия. Только лучше.
.
Лео
Ньютон
Яркие
Мягкие

Задача выполнимости булевых формул

Из Википедии — свободной энциклопедии

Запрос «3SAT» перенаправляется сюда; о немецко-австрийско-швейцарском телеканале см. 3sat.

Зада́ча выполни́мости бу́левых фо́рмул (SAT или ВЫП) — важная для теории вычислительной сложности алгоритмическая задача.

Экземпляром задачи SAT является булева формула, состоящая только из имен переменных, скобок и операций (И), (ИЛИ) и (HE). Задача заключается в следующем: можно ли назначить всем переменным, встречающимся в формуле, значения ложь и истина так, чтобы формула стала истинной.

Согласно теореме Кука, доказанной Стивеном Куком в 1971 году, задача SAT для булевых формул, записанных в конъюнктивной нормальной форме, является NP-полной. Требование о записи в конъюнктивной форме существенно, так как, например, задача SAT для формул, представленных в дизъюнктивной нормальной форме, тривиально решается за линейное время в зависимости от размера записи формулы (для выполнимости формулы требуется только наличие хотя бы одной конъюнкции, не содержащей одновременно x и NOT x для некоторой переменной x).

Точная формулировка

Чтобы чётко сформулировать задачу распознавания, необходимо условиться об алфавите, с помощью которого задаются экземпляры языка. Этот алфавит должен быть фиксирован и конечен. В своей книге Хопкрофт, Мотвани и Ульман предлагают использовать следующий алфавит: {«», «», «», «», «», «», «», «»}.

При использовании такого алфавита скобки и операторы записываются естественным образом, а переменные получают следующие имена: x1, x10, x11, x100 и т. д., согласно их номерам, записанным в двоичной системе счисления.

Пусть некоторая булева формула, записанная в обычной математической нотации, имела длину символов. В ней каждое вхождение каждой переменной было описано хотя бы одним символом, следовательно, всего в данной формуле не более переменных. Значит, в предложенной выше нотации каждая переменная будет записана с помощью символов. В таком случае, вся формула в новой нотации будет иметь длину символов, то есть длина строки возрастет в полиномиальное число раз.

Например, формула примет вид .

Вычислительная сложность

В 1970-м году в статье Стивена Кука был впервые введен термин «NP-полная задача», и задача SAT была первой задачей, для которой доказывалось это свойство.

В доказательстве теоремы Кука каждая задача из класса NP в явном виде сводится к SAT. После появления результатов Кука была доказана NP-полнота для множества других задач. При этом чаще всего для доказательства NP-полноты некоторой задачи приводится полиномиальная сводимость задачи SAT к данной задаче, возможно в несколько шагов, то есть с использованием нескольких промежуточных задач.

Частные случаи задачи SAT

Интересными важными частными случаями задачи SAT являются:

  • Задача выполнимости булевых формул в конъюнктивной нормальной форме (SATCNF или ВКНФ) — аналогичная задача, с наложенным на формулу условием: она должна быть записана в конъюнктивной нормальной форме. Задача ВКНФ также NP-полна.
  • Задача выполнимости булевых формул в k-конъюнктивной нормальной форме (k-SAT или k-ВЫП) — задача выполнимости при условии, что формула записана в k-конъюнктивной нормальной форме. Эта задача является NP-полной при .
  • Задача выполнимости булевых формул в 2-конъюнктивной нормальной форме имеет полиномиальное решение, то есть принадлежит классу P.

CDCL-решатели

Основная статья: Алгоритм CDCL

Одним из наиболее эффективных методов распараллеливания задач SAT являются CDCL-решатели (CDCL, англ. conflict-driven clause learning), основывающиеся на нехронологических вариантах алгоритма DPLL[1][2].

См. также

Примечания

  1. Marques-Silva J. P. GRASP: A search algorithm for propositional satisfiability / J. P. Marques-Silva, K. A. Sakallah // IEEE Transactions on Computers. — 1999. — Vol. 48, N 5. — P. 506—521.
  2. Семенов А. А., Заикин О. С. Алгоритмы построения декомпозиционных множеств для крупноблочного распараллеливания SAT-задач. Серия «Математика» 2012. Т. 5, No 4. С. 79—94

Ссылки

Эта страница в последний раз была отредактирована 6 февраля 2021 в 20:36.
Основа этой страницы находится в Википедии. Текст доступен по лицензии CC BY-SA 3.0 Unported License. Нетекстовые медиаданные доступны под собственными лицензиями. Wikipedia® — зарегистрированный товарный знак организации Wikimedia Foundation, Inc. WIKI 2 является независимой компанией и не аффилирована с Фондом Викимедиа (Wikimedia Foundation).