Изменения

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

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

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

*<tex>(\Rightarrow)</tex>Докажем достаточность: Пусть 2-SAT имеет решение. Докажем, что не может быть такого, чтобы для любой переменной <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 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> \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>. Противоречие.

*#Построим граф импликаций.*#[http://e-maxx.ru/algo/strong_connected_components Найдём в этом графе компоненты сильной связности за время <tex>O(N + 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>. Если это условие не выполняется, то вернуть "решение не существует".*#Если <tex>comp[x] > comp[\overline x]</tex>, то переменной x выбираем значение true, иначе - false. == Применение 2-SAT задач == Предположим, что семь комиков согласились во время трехдневного фестиваля дать концерты в двух из пяти отелей. При этом у каждого из них один из дней занят другой работой, поэтому вот как выглядят возможные варианты их выступлений в отелях Лас-Вегаса:  *Tomlin может выступить в отелях Aladdin и Caesars в дни 1 и 2;*Unwin может выступить в отелях Bellagio и Excalibur в дни 1 и 2;*Vegas может выступить в отелях Desert и Excalibur в дни 2 и 3;*Williams может выступить в отелях Aladdin и Desert в дни 1 и 3;*Xie может выступить в отелях Caesars и Excalibur в дни 1 и 3;*Yankovic может выступить в отелях Bellagio и Desert в дни 2 и 3;*Zany может выступить в отелях Bellagio и Caesars в дни 1 и 2.  Можно ли составить расписание так, чтобы не возникало никаких конфликтов?Для решения этой задачи можно ввести семь булевых переменных <tex>{t, u, v, w, x, у, z}, </tex> где <tex>t</tex> например, означает выступление Tomlin в Aladdin в первый день и в Caesars во второй, в то время как <tex> \overline t </tex> означает, что дни соответствуют отелям в обратном порядке: выступление в Aladdin — во второй день, а в Caesars — в первый. Тогда мы можем записать ограничения, означающие, что никакие два комедианта не выступают в одном отеле в один и тот же день, следующим образом.  Тогда мы можем записать ограничения, означающие, что никакие два комедианта не выступают в одном отеле в один и тот же день, следующим образом. (В квадратных скобках указаны первая буква отеля и день, в который двое участников не могут выступать одновременно). {| class="wikitable" style="width:10cm" border=1 |<tex>\overline {(t \wedge w)} {[}A1{]} </tex> ||<tex>\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] </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 </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)</tex> Кроме того, дизъюнкты Крома могут быть записаны в виде импликаций:  <tex> (t \to \overline w) \wedge (u \to \overline z) \wedge (\overline u \to \overline y) \wedge (\overline u \to z) \wedge (y \to z) \wedge (\overline t \to \overline x) \wedge (\overline t \to z) \wedge (x \to z) \wedge</tex> <tex> (t \to \overline z) \wedge (v \to y) \wedge (\overline v \to \overline w) \wedge (\overline v \to \overline y) \wedge (w \to \overline y) \wedge (\overline u \to x) \wedge (u \to v) \wedge (v \to \overline x)</tex> И каждая такая импликация может также быть представлена в альтернативном, "контрапозитивном" виде: <tex> (w \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 \to u) \wedge (x \to \overline v)</tex> При решение данной задачи можно найти следующий цикл: <tex> u \to \overline z \to \overline y \to \overline v \to \overline u \to z \to \overline t \to \overline x \to \overline u</tex> Этот цикл говорит о том, что <tex> v </tex> и <tex> \overline v </tex> должны иметь одно и то же значение; так что нет никакой возможности удовлетворить все условия. Если расписание должно быть составлено любой ценой, организаторам фестиваля придется провести переговоры и пересмотреть соглашение по крайней мере с одним из семи комедиантов.

Организаторы могут, например, попытаться временно вывести Компоненты сильной связности найдем за рамки картины <tex> v O(N + M)</tex>. Тогда пять из шестнадцати ограничений исчезнут, и останутся только 22 затем проверим каждую из импликаций.Такое решение будет иметь циклы наподобие <tex> z \to \overline u \to x \to z N</tex> или переменных за <tex> t \to \overline z \to t O(N)</tex>. Можно заметить что значение Следовательно асимптотика <tex> tuwxyz = 110000 O(N + M)</tex> выполняют каждый дизъюнкт. Эти значения дают нам расписание, которое выполняет шесть из семи исходных условий, начиная с выступления (Tomlin, Unwin, Zany, Williams, Xie) в первый день в (Aladdin, Bellagio, Caesars, Desert, Excalibur).

*[https://en.wikipedia.org/wiki/2-satisfiability 2-satisfiability - — Википедия]