Задача выполнимости булевых формул
Зада́ча выполни́мости бу́левых фо́рмул (SAT или ВЫП) — важная для теории вычислительной сложности алгоритмическая задача.
Экземпляром задачи SAT является булева формула, состоящая только из имен переменных, скобок и операций <math>\wedge</math> (И), <math>\vee</math> (ИЛИ) и <math>\neg</math> (HE). Задача заключается в следующем: можно ли назначить всем переменным, встречающимся в формуле, значения ложь и истина так, чтобы формула стала истинной.
Согласно теореме Кука, доказанной Стивеном Куком в 1971 году, задача SAT для булевых формул, записанных в конъюнктивной нормальной форме, является NP-полной. Требование о записи в конъюнктивной форме существенно, так как, например, задача SAT для формул, представленных в дизъюнктивной нормальной форме, тривиально решается за линейное время в зависимости от размера записи формулы (для выполнимости формулы требуется только наличие хотя бы одной конъюнкции, не содержащей одновременно x и NOT x для некоторой переменной x).
Содержание
Точная формулировка
Чтобы чётко сформулировать задачу распознавания, необходимо условиться об алфавите, с помощью которого задаются экземпляры языка. Этот алфавит должен быть фиксирован и конечен. В своей книге Хопкрофт, Мотвани и Ульман предлагают использовать следующий алфавит: {"<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 и т. д., согласно их номерам, записанным в двоичной системе счисления.
Пусть некоторая булева формула, записанная в обычной математической нотации, имела длину <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>.
Вычислительная сложность
В 1970-м году в статье Стивена Кука был впервые введен термин «NP-полная задача», и задача SAT была первой задачей, для которой доказывалось это свойство.
В доказательстве теоремы Кука каждая задача из класса NP в явном виде сводится к SAT. После появления результатов Кука была доказана NP-полнота для множества других задач. При этом чаще всего для доказательства NP-полноты некоторой задачи приводится полиномиальное сведение задачи SAT к данной задаче, возможно в несколько шагов, то есть с использованием нескольких промежуточных задач.
Частные случаи задачи SAT
Интересными важными частными случаями задачи SAT являются:
- Задача выполнимости булевых формул в конъюнктивной нормальной форме (SATCNF или ВКНФ) — аналогичная задача, с наложенным на формулу условием: она должна быть записана в конъюнктивной нормальной форме. Задача ВКНФ также NP-полна.
- Задача выполнимости булевых формул в k-конъюнктивной нормальной форме (k-SAT или k-ВЫП) — задача выполнимости при условии, что формула записана в k-конъюнктивной нормальной форме. Эта задача является NP-полной при <math>k\geq 3</math>.
- Задача выполнимости булевых формул в 2-конъюнктивной нормальной форме имеет полиномиальное решение, то есть принадлежит классу P.
CDCL-решатели
Одним из наиболее эффективных методов распараллеливания задач SAT являются CDCL-решатели (CDCL, англ. conflict-driven clause learning), основывающиеся на нехронологических вариантах алгоритма DPLL[1][2].
См. также
Напишите отзыв о статье "Задача выполнимости булевых формул"
Примечания
- ↑ 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.
- ↑ Семенов А. А., Заикин О. С. Алгоритмы построения декомпозиционных множеств для крупноблочного распараллеливания SAT-задач. Серия «Математика» 2012. Т. 5, No 4. С. 79—94
Ссылки
- [www.satcompetition.org/ The international SAT Competitions web page]
- [www.satlib.org/ SATLIB — The Satisfiability Library]
- [www.satlive.org/ Sat Live] — общий сайт о SAT.
| ||||||||||||||||||||||||||||||||||
Отрывок, характеризующий Задача выполнимости булевых формул
– Я никогда не радовалась тогда, – сказала графиня, – когда Болконский был женихом Наташи, а я всегда желала, и у меня есть предчувствие, что Николинька женится на княжне. И как бы это хорошо было!Соня чувствовала, что это была правда, что единственная возможность поправления дел Ростовых была женитьба на богатой и что княжна была хорошая партия. Но ей было это очень горько. Несмотря на свое горе или, может быть, именно вследствие своего горя, она на себя взяла все трудные заботы распоряжений об уборке и укладке вещей и целые дни была занята. Граф и графиня обращались к ней, когда им что нибудь нужно было приказывать. Петя и Наташа, напротив, не только не помогали родителям, но большею частью всем в доме надоедали и мешали. И целый день почти слышны были в доме их беготня, крики и беспричинный хохот. Они смеялись и радовались вовсе не оттого, что была причина их смеху; но им на душе было радостно и весело, и потому все, что ни случалось, было для них причиной радости и смеха. Пете было весело оттого, что, уехав из дома мальчиком, он вернулся (как ему говорили все) молодцом мужчиной; весело было оттого, что он дома, оттого, что он из Белой Церкви, где не скоро была надежда попасть в сраженье, попал в Москву, где на днях будут драться; и главное, весело оттого, что Наташа, настроению духа которой он всегда покорялся, была весела. Наташа же была весела потому, что она слишком долго была грустна, и теперь ничто не напоминало ей причину ее грусти, и она была здорова. Еще она была весела потому, что был человек, который ею восхищался (восхищение других была та мазь колес, которая была необходима для того, чтоб ее машина совершенно свободно двигалась), и Петя восхищался ею. Главное же, веселы они были потому, что война была под Москвой, что будут сражаться у заставы, что раздают оружие, что все бегут, уезжают куда то, что вообще происходит что то необычайное, что всегда радостно для человека, в особенности для молодого.
31 го августа, в субботу, в доме Ростовых все казалось перевернутым вверх дном. Все двери были растворены, вся мебель вынесена или переставлена, зеркала, картины сняты. В комнатах стояли сундуки, валялось сено, оберточная бумага и веревки. Мужики и дворовые, выносившие вещи, тяжелыми шагами ходили по паркету. На дворе теснились мужицкие телеги, некоторые уже уложенные верхом и увязанные, некоторые еще пустые.
Голоса и шаги огромной дворни и приехавших с подводами мужиков звучали, перекликиваясь, на дворе и в доме. Граф с утра выехал куда то. Графиня, у которой разболелась голова от суеты и шума, лежала в новой диванной с уксусными повязками на голове. Пети не было дома (он пошел к товарищу, с которым намеревался из ополченцев перейти в действующую армию). Соня присутствовала в зале при укладке хрусталя и фарфора. Наташа сидела в своей разоренной комнате на полу, между разбросанными платьями, лентами, шарфами, и, неподвижно глядя на пол, держала в руках старое бальное платье, то самое (уже старое по моде) платье, в котором она в первый раз была на петербургском бале.
Наташе совестно было ничего не делать в доме, тогда как все были так заняты, и она несколько раз с утра еще пробовала приняться за дело; но душа ее не лежала к этому делу; а она не могла и не умела делать что нибудь не от всей души, не изо всех своих сил. Она постояла над Соней при укладке фарфора, хотела помочь, но тотчас же бросила и пошла к себе укладывать свои вещи. Сначала ее веселило то, что она раздавала свои платья и ленты горничным, но потом, когда остальные все таки надо было укладывать, ей это показалось скучным.
– Дуняша, ты уложишь, голубушка? Да? Да?
И когда Дуняша охотно обещалась ей все сделать, Наташа села на пол, взяла в руки старое бальное платье и задумалась совсем не о том, что бы должно было занимать ее теперь. Из задумчивости, в которой находилась Наташа, вывел ее говор девушек в соседней девичьей и звуки их поспешных шагов из девичьей на заднее крыльцо. Наташа встала и посмотрела в окно. На улице остановился огромный поезд раненых.
Девушки, лакеи, ключница, няня, повар, кучера, форейторы, поваренки стояли у ворот, глядя на раненых.
Наташа, накинув белый носовой платок на волосы и придерживая его обеими руками за кончики, вышла на улицу.
Бывшая ключница, старушка Мавра Кузминишна, отделилась от толпы, стоявшей у ворот, и, подойдя к телеге, на которой была рогожная кибиточка, разговаривала с лежавшим в этой телеге молодым бледным офицером. Наташа подвинулась на несколько шагов и робко остановилась, продолжая придерживать свой платок и слушая то, что говорила ключница.
