Изменения

|definition = 2-SAT <b><tex>\mathrm {2SAT}</tex></b> (2-satisfiability) выполнимость данной функции — задача распределения аргументов в булевой [[КНФ|КНФ]] функции, записанной в виде [[Специальные_формы_КНФ|2-КНФ (КНФ Крома)]], таким образом, чтобы результат данной функции был равен <tex> 1 </tex>.

== Алгоритм Решения решения ==

Несложно заметить, что это равнозначно записи <tex>(\overline a \to b \wedge \overline b \to \overline a) </tex>.

Построим [[Основные_определения_теории_графов|ориентированный граф]], где вершинами будут аргументы и их отрицание, а ребрами будут ребра вида: <tex>\overline a \to b </tex> и <tex> \overline b \to \overline a </tex> для каждого дизъюнкта функции <tex> a \vee b </tex>.

Для того, чтобы данная задача 2-SAT <tex>\mathrm {2SAT}</tex> имела решение, необходимо и достаточно, чтобы для любой переменной <tex> x </tex> из вершины <tex> x </tex> нельзя достичь <tex> \overline x </tex> и из вершины <tex> \overline x </tex> нельзя достичь <tex> x </tex> одновременно. <tex>(\overline x \to x ) \wedge (x \to \overline x) </tex>.

*<tex>(\Rightarrow)</tex>Докажем достаточность: Пусть 2-SAT <tex>\mathrm {2SAT}</tex> имеет решение. Докажем, что не может быть такого, чтобы для любой переменной <tex> x </tex> из вершины <tex> x </tex> можно достичь <tex> \overline x </tex> и из вершины <tex> \overline x </tex> можно достичь <tex> x </tex> одновременно. <tex>((\overline x \to x ) \wedge (x \to \overline x)) </tex>. Тогда чтобы из <tex> \overline x </tex> достичь <tex> x </tex> <tex> (\overline x \to x </tex> было верным), <tex> x </tex> должен быть равен <tex> 1 </tex>. С другой стороны для того, чтобы из <tex> x </tex> достичь <tex> \overline x </tex> <tex> (\overline x \to \overline x </tex> было верным), <tex> x </tex> должен быть равен 0. Отсюда следует противоречие.

*<tex>(\Leftarrow)</tex>Докажем необходимость: Пусть для любой переменной <tex> x </tex> из вершины <tex> x </tex> нельзя достичь <tex> \overline x </tex> и из вершины <tex> \overline x </tex> нельзя достичь <tex> x </tex> одновременно. Докажем, что этого достаточно, чтобы 2-SAT <tex>\mathrm {2SAT}</tex> имело решение. Пусть из <tex> \overline x </tex> можно достичь <tex> x </tex>, но из вершины <tex> x </tex> нельзя достичь <tex> \overline x </tex>. Докажем, что из <tex> x </tex> не достижимо такой <tex> y </tex>, что из <tex> y </tex> достижимо <tex> \overline y </tex>. (т.е. <tex> x \to y \to \overline y \, (x = 1, y = 0)) </tex>. Если из <tex> x \to y </tex>, то <tex> \overline x \vee y </tex>, отсюда следует <tex> \overline y \to \overline x </tex>. Тогда <tex> x \to y \to \overline y \to \overline x </tex>. Следовательно <tex> x \to \overline x </tex>. Противоречие.

*#Построим граф импликаций.*#<i>Найдём в этом графе [[Отношение_связности,_компоненты_связности#Сильная связность | компоненты сильной связности ]] за время <tex>O(N + M)</tex></i>, пусть где <tex> N </tex> — количество вершин в графе (удвоенное количество переменных), а <tex> M </tex> — количество ребер графа (удвоенное количество дизъюнктов).#Пусть <tex>comp[v]</tex> — это номер компоненты сильной связности, которой принадлежит вершина вершине <tex>v</tex>.*Проверим, что для каждой переменной <tex>x</tex> вершины <tex>x</tex> и <tex>\overline x</tex> лежат в разных компонентах, т.е. <tex>comp[x] \ne comp[\overline x]</tex>. Если это условие не выполняется, то вернуть "<i>решение не существует"</i>.*#Если <tex>comp[x] > comp[\overline x]</tex>, то переменной <tex>x </tex> выбираем значение <tex> \mathtt {true}</tex>, иначе - — <tex> \mathtt {false}</tex>. Компоненты сильной связности найдем за <tex>O(N + M)</tex>, затем проверим каждую из <tex>N</tex> переменных за <tex>O(N)</tex>. Следовательно асимптотика <tex>O(N + M)</tex>.

== Применение 2-SAT задач Примеры решения 2SAT == === Первый пример ===

Предположим, что семь комиков согласились во время трехдневного фестиваля дать концерты в двух из пяти отелей. При этом у каждого из них один из дней занят другой работой, поэтому вот как выглядят возможные варианты их выступлений в отелях Лас-ВегасаРассмотрим следующую функцию: <tex> (a \vee b) \wedge (a \vee c) \wedge(\overline b \vee c) \wedge(\overline b \vee a) </tex>

*Tomlin может выступить в отелях Aladdin и Caesars в дни 1 и 2;Данная функция эквивалентна функции *Unwin может выступить в отелях Bellagio и Excalibur в дни 1 и 2;<tex>*Vegas может выступить в отелях Desert и Excalibur в дни 2 и 3;\overline a \to b \wedge*Williams может выступить в отелях Aladdin и Desert в дни 1 и 3;\overline b \to a \wedge*Xie может выступить в отелях Caesars и Excalibur в дни 1 и 3;\overline a \to c \wedge*Yankovic может выступить в отелях Bellagio и Desert в дни 2 и 3;\overline c \to a \wedge*Zany может выступить в отелях Bellagio и Caesars в дни 1 и 2b \to c \wedge\overline c \to \overline b \wedge\overline a \to \overline b \wedgea \to b</tex>.

Можно ли составить расписание так, чтобы не возникало никаких конфликтов?Построим ориентированный граф со следующими множествами вершинам и ребер:Для решения этой задачи можно ввести семь булевых переменных множество вершин <tex>V = \{ta, ub, vc, w\overline a, x\overline b, у, z\overline c\}, </tex> где множество ребер <tex>t</tex> напримерE = \{(\overline a, b), (\overline b, a), (\overline a, c), (\overline c, a), (b, означает выступление Tomlin в Aladdin в первый день и в Caesars во второйc), в то время как <tex> (\overline t </tex> означаетc, что дни соответствуют отелям в обратном порядке: выступление в Aladdin — во второй день\overline b), а в Caesars — в первый. Тогда мы можем записать ограничения(\overline a, означающие\overline b), что никакие два комедианта не выступают в одном отеле в один и тот же день(b, следующим образомa)\}</tex>.

Тогда мы можем записать ограничения, означающие, что никакие два комедианта не выступают Рассмотрим в одном отеле в один и тот же день, следующим образом. (В квадратных скобках указаны первая буква отеля и день, в который двое участников не могут выступать одновременно)графе следующие пути:* <tex> \overline a \to b \to a </tex>* <tex> \overline a \to \overline b \to a </tex>* <tex> \overline c \to a </tex>* <tex> a \to c </tex>* <tex> \overline a \to b \to c </tex>.

{| class="wikitable" style="width:10cm" border=1 |Т.к. <tex>\overline {(t a \wedge w)} {[}A1{]} to a </tex> ||, то <tex>a = 1, \overline {(y \wedge \overline z)} {[}B2{]} </tex> ||<tex>\overline {(t \wedge z)} {[}C2{]} </tex> ||<tex>\overline {(w \wedge y)} {[}D3{]} </tex> |- |<tex>\overline {(u \wedge z)} {[}B1{]} </tex> ||<tex>\overline {(\overline t \wedge x)} {[}C1{]} </tex> ||<tex>\overline {(v \wedge \overline y)} {[}D2{]} </tex> ||<tex>\overline {(\overline u \wedge \overline x)} {[}E1{]} </tex> |- |<tex>\overline {(\overline u \wedge y)} [B2] </tex> ||<tex>\overline {(\overline t \wedge \overline z)} [C1] </tex> ||<tex>\overline {(\overline v \wedge w)} [D3] </tex> ||<tex>\overline {(u \wedge \overline v)} [E2] </tex> |- |<tex>\overline {(\overline u \wedge \overline z)} [B2] </tex> ||<tex>\overline {(x \wedge \overline z)} [C1] </tex> ||<tex>\overline {(\overline v \wedge y)} [D3] </tex> ||<tex>\overline {(v \wedge x)} [E3] a = 0 </tex>|}.

Каждое из этих ограниченийТ.к. <tex> a \to c </tex> и <tex> a = 1 </tex>, конечно жето <tex> c = 1, представляет собой дизъюнкт Крома, которые мы должны выполнить\overline c = 0 </tex>.

Значения <tex> (\overline t \vee \overline w) \wedge (\overline u \vee \overline z) \wedge (u \vee \overline y) \wedge (u \vee z) \wedge (\overline y \vee z) \wedge (t \vee \overline x) \wedge (t \vee z) \wedge (\overline x \vee z) \wedge b </tex>может быть любым, т.к. все вершины, из которых можно добраться в <tex> b </tex> имеют значение ноль.

<b> Ответ: </b> <tex> a = 1, b = 0, c = 1 </tex> или <tex> (\overline t \vee \overline z) \wedge (\overline v \vee y) \wedge (v \vee \overline w) \wedge (v \vee \overline y) \wedge (\overline w \vee \overline y) \wedge (u \vee x) \wedge (\overline u \vee v) \wedge (\overline v \vee \overline x)a = 1, b = 1, c = 1 </tex>.

Рассмотрим следующую функцию: <tex> (t \to overline a \overline wvee c) \wedge (u \to \overline z) \wedge (\overline u c \to vee \overline ya) \wedge (\overline u \to z) \wedge (y a \to zvee b) \wedge (\overline t \to \overline x) \wedge (\overline t b \to zvee a) \wedge (x \to z) \wedge

(t a \to \overline z) c \wedge (v \to y) \wedge (\overline v c \to \overline w) a \wedge (\overline v c \to \overline y) a \wedge (w a \to \overline y)c \wedge \overline a \to b \wedge (\overline u b \to x) a \wedge (u b \to v)a \wedge \wedge (v overline b \to \overline x)a

И каждая такая импликация может также быть представлена в альтернативномПостроим ориентированный граф со следующими множествами вершинам и ребер:множество вершин V = <tex>\{a, b, c, \overline a, \overline b, \overline c\}, </tex>множество ребер <tex> E = \{(a, c), (\overline c, \overline a), (c, \overline a), (a, \overline c), (\overline a, b), (\overline b, a), (b, a), (\overline b, "контрапозитивном" виде\overline a)\}</tex>. Заметим следующий путь:<tex> a \to c \to \overline a \to b \to a </tex>.

Отсюда следует, что <tex> (w a \to \overline t) \wedge (z \to \overline u) \wedge (\overline y \to \overline u) \wedge (\overline z \to u) \wedge (z \to y) \wedge (\overline x \to \overline t) \wedge (\overline z \to t) \wedge (z \to x) \wedge </tex><tex> (z \to \overline t) \wedge (y \to v) \wedge (\overline w \to \overline v) \wedge (\overline y \to \overline v) \wedge (y \to \overline w) \wedge (\overline u \to x) \wedge (v a \to u) \wedge (x \to \overline v)a </tex>.

При решение Следовательно по ранее доказанной теореме, у данной задачи можно найти следующий цикл:функции решений нет.

<texb> u \to \overline z \to \overline y \to \overline v \to \overline u \to z \to \overline t \to \overline x \to \overline uОтвет: </texb>Решений нет.

Организаторы могут, например, попытаться временно вывести за рамки картины Решение <tex> v \mathrm {2SAT}</tex>может потребоваться в следующих задачах: *латинские квадраты<ref> [https://ru.wikipedia. Тогда пять из шестнадцати ограничений исчезнутorg/wiki/Латинский_квадрат Википедия — Латинские квадраты] </ref>, и останутся только 22 из импликаций.Такое решение будет иметь циклы наподобие *квазигруппы<texref> z \to \overline u \to x \to z [https://ru.wikipedia.org/wiki/Квазигруппа_(социология) Википедия — Квазигруппы]</texref> или ,*числа Рамсея<texref> t \to \overline z \to t [https://ru.wikipedia.org/wiki/Теорема_Рамсея#.D0.A7.D0.B8.D1.81.D0.BB.D0.B0_.D0.A0.D0.B0.D0.BC.D1.81.D0.B5.D1.8F Википедия — Числа Рамсея]</texref>. ,Можно заметить что значение *система Штейнера<texref> tuwxyz = 110000 [https://ru.wikipedia.org/wiki/Система_Штейнера Википедия — Система Штейнера]</texref> выполняют каждый дизъюнкт. Эти значения дают нам расписание, которое выполняет шесть из семи исходных условий*проектирование протоколов (пример: для сетевых коммуникаций), начиная с выступления *электронная коммерция (TomlinЭлектронные аукционы и автоматизированные брокеры, Unwin*теории кодирования, Zanyкриптографии, Williams, Xie) в первый день в *проектирование и тестирование лекарств (Aladdin, Bellagio, Caesars, Desert, Excaliburмед. препаратов).

*[http:== Примечания ==<references//e-maxx.ru/algo/strong_connected_components MAXimal :: algo :: Поиск компонент сильной связности за O(N + M)] >

*[http://e-maxx.ru/algo/2_sat MAXimal :: algo :: Задача 2-SAT 2SAT (2-CNF) ]*[https://en.wikipedia.org/wiki/2-satisfiability Википедия — 2-satisfiability - Википедия]