Изменения

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

Рассмотрим {{Теорема|statement=Для того, чтобы данная задача <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 (a x \to \overline x) </tex>.|| bproof=<tex>(\Rightarrow) <br/tex>Докажем достаточность: Пусть <tex>\mathrm {2SAT}</tex>Несложно заметить имеет решение. Докажем, что это равнозначно записи !a =не может быть такого, чтобы для любой переменной <tex> x </tex> из вершины <tex> x </tex> можно достичь <tex> \overline x </tex> b и !b =из вершины <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> (x \to \overline x </tex> было верным), <tex> a x <br/tex>должен быть равен 0. Отсюда следует противоречие.

Построим ориентированный граф<tex>(\Leftarrow)</tex>Докажем необходимость: Пусть для любой переменной <tex> x </tex> из вершины <tex> x </tex> нельзя достичь <tex> \overline x </tex> и из вершины <tex> \overline x </tex> нельзя достичь <tex> x </tex> одновременно. Докажем, что этого достаточно, чтобы <tex>\mathrm {2SAT}</tex> имело решение. Пусть из <tex> \overline x </tex> можно достичь <tex> x </tex>, но из вершины <tex> x </tex> нельзя достичь <tex> \overline x </tex>. Докажем, где вершинами будут аргументы и их отрицаниечто из <tex> x </tex> не достижимо такой <tex> y </tex>, а ребрами будут ребра вида: !a =что из <tex> y </tex> достижимо <tex> \overline y </tex> b и !b =. (т.е. <tex> a для каждого дизъюнкта функции x \to y \to \overline y\, (a || bx = 1, y = 0)) <br/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>. Противоречие.}}

Пусть 2-SAT имеет решение. <br>== Примеры решения 2SAT == Докажем, что не может быть такого, чтобы для любой переменной x из вершины x можно достичь !x и из вершины !x можно достичь x одновременно. (!x => x && x => !x) <br>Тогда чтобы из !x достичь x (!x => x) x было верным, x должен быть равен 1. С другой стороны для того, чтобы из x достичь !x (!x Первый пример ===> x) было верным, x должен быть равен 0. Отсюда следует противоречие. <br> <br>

Пусть для любой переменной x из вершины x нельзя достичь !x и из вершины !x нельзя достичь x одновременно. Рассмотрим следующую функцию: <brtex>(a \vee b) \wedge Докажем, что этого достаточно, чтобы 2-SAT имело решение. <br>Пусть из !x можно достичь x, но из вершины x нельзя достичь !x. Докажем, что из x не достижимо такой y, что из y достижимо !y. (т.е. x => y => !y. (x = 1, y = 0)a \vee c). <br>\wedgeЕсли из x => y, то (!x || y\overline b \vee c), отсюда следует \wedge(!y => !x\overline b \vee a). Тогда x => y => !y => !x. Следовательно x =</tex> !x. Противоречие.

Построим ориентированный граф со следующими множествами вершинам и ребер:множество вершин <tex> V = \{a, b, c, \overline a, \overline b, \overline c\}, </tex>множество ребер <tex> E = \{(\overline a, b), (\overline b, a), (\overline a, c), (\overline c, a), (b, c), (\overline c, \overline b), (\overline a, \overline b), (a, b)\}</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>. Т.к. <tex> \overline a \to a </tex>, то <tex> a = 1, \overline a = 0 </tex>. Т.к. <tex> a \to c </tex> и <tex> a = 1 </tex>, то <tex> c = 1, \overline c = 0 </tex>. Значения <tex> b </tex> может быть любым, т.к. все вершины, из которых можно добраться в <tex> b </tex> имеют значение ноль. <b> Ответ: </b> <tex> a = 1, b = 0, c = 1 </tex> или <tex> a = 1, b = 1, c = 1 </tex>. === Второй пример === Рассмотрим следующую функцию: <tex>(\overline a \vee c) \wedge(\overline c \vee \overline a) \wedge(a \vee b) \wedge(\overline b \vee a)</tex> Данная функция эквивалентна функции <tex>a \to c \wedge\overline c \to \overline a \wedgec \to \overline a \wedgea \to \overline c \wedge\overline a \to b \wedge\overline b \to a \wedgeb \to a \wedge\overline b \to \overline a</tex> Построим ориентированный граф со следующими множествами вершинам и ребер:множество вершин 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> a \to \overline a \to a </tex>. Следовательно по ранее доказанной теореме, у данной функции решений нет. <b> Ответ: </b> Решений нет. == Использование 2SAT == Решение <tex>\mathrm {2SAT}</tex> может потребоваться в следующих задачах: *латинские квадраты<ref> [https://ru.wikipedia.org/wiki/Латинский_квадрат Википедия — Латинские квадраты] </ref>, *квазигруппы<ref>[https://ru.wikipedia.org/wiki/Квазигруппа_(социология) Википедия — Квазигруппы]</ref>,*числа Рамсея<ref>[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 Википедия — Числа Рамсея]</ref>,*система Штейнера<ref>[https://ru.wikipedia.org/wiki/Система_Штейнера Википедия — Система Штейнера]</ref>,*проектирование протоколов (пример: для сетевых коммуникаций),*электронная коммерция (Электронные аукционы и автоматизированные брокеры,*теории кодирования, криптографии,*проектирование и тестирование лекарств (мед. препаратов). == См. также == *[[3CNFSAT | NP-полнота задачи о выполнимости булевой формулы в форме 3-КНФ]] == Примечания ==<references/> == Источники информации == *[http://e-maxx.ru/algo/2_sat MAXimal :: algo :: Задача 2-SAT 2SAT (2-CNF) ]*[https://en.wikipedia.org/wiki/2-satisfiability Википедия — 2-satisfiability] [[Категория: Дискретная математика и алгоритмы]] [[Категория: Булевы функции ]]