Викиконспекты - Вклад участника [ru]

2SAT

2016-01-18T17:04:26Z

GARiK Carrot:

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

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

Рассмотрим любой дизъюнкт функции: <tex> a \vee b </tex>.
Несложно заметить, что это равнозначно записи <tex>(\overline a \to b \wedge b \to \overline a) </tex>.

Построим [[Основные_определения_теории_графов|ориентированный граф]], где вершинами будут аргументы и их отрицание, а ребрами будут ребра вида: <tex>\overline a \to b </tex> и <tex> b \to \overline a </tex> для каждого дизъюнкта функции <tex> a \vee b </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 x \to \overline x) </tex>.
|proof=
<tex>(\Rightarrow)</tex>Докажем достаточность: Пусть <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 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> одновременно. Докажем, что этого достаточно, чтобы <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>. Противоречие.
}}

Теперь мы можем собрать весь алгоритм воедино:

#Построим граф импликаций.
#Найдём в этом графе [[Отношение_связности,_компоненты_связности#Сильная связность | компоненты сильной связности]] за время <tex>O(N + M)</tex>, где <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>. Если это условие не выполняется, то вернуть решение не существует.
#Если <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>.

== Примеры решения 2SAT ==
=== Первый пример ===

Рассмотрим следующую функцию: <tex> (a \vee b) \wedge
(a \vee c) \wedge
(\overline b \vee c) \wedge
(\overline b \vee a) </tex>

Данная функция эквивалентна функции
<tex>
\overline a \to b \wedge
\overline b \to a \wedge
\overline a \to c \wedge
\overline c \to a \wedge
b \to c \wedge
\overline c \to \overline b \wedge
\overline a \to \overline b \wedge
a \to b
</tex>.

Построим ориентированный граф со следующими множествами вершинам и ребер:
множество вершин <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> имеют значение ноль.

 Ответ: <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 \wedge
c \to \overline a \wedge
a \to \overline c \wedge
\overline a \to b \wedge
\overline b \to a \wedge
b \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>.

Следовательно по ранее доказанной теореме, у данной функции решений нет.

 Ответ: Решений нет.

== Использование 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 :: Задача 2SAT (2-CNF) ]
*[https://en.wikipedia.org/wiki/2-satisfiability Википедия — 2-satisfiability]

[[Категория: Дискретная математика и алгоритмы]]

[[Категория: Булевы функции ]]

2SAT

2016-01-18T16:54:16Z

GARiK Carrot: Исправлены примечания

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

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

Рассмотрим любой дизъюнкт функции: <tex> a \vee b </tex>.
Несложно заметить, что это равнозначно записи <tex>(\overline a \to b \wedge b \to \overline a) </tex>.

Построим [[Основные_определения_теории_графов|ориентированный граф]], где вершинами будут аргументы и их отрицание, а ребрами будут ребра вида: <tex>\overline a \to b </tex> и <tex> b \to \overline a </tex> для каждого дизъюнкта функции <tex> a \vee b </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 x \to \overline x) </tex>.
|proof=
<tex>(\Rightarrow)</tex>Докажем достаточность: Пусть <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 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> одновременно. Докажем, что этого достаточно, чтобы <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>. Противоречие.
}}

Теперь мы можем собрать весь алгоритм воедино:

#Построим граф импликаций.
#Найдём в этом графе [[Отношение_связности,_компоненты_связности#Сильная связность | компоненты сильной связности]] за время <tex>O(N + M)</tex>, где <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>. Если это условие не выполняется, то вернуть "решение не существует".
#Если <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>.

== Примеры решения 2SAT ==
=== Первый пример ===

Рассмотрим следующую функцию: <tex> (a \vee b) \wedge
(a \vee c) \wedge
(\overline b \vee c) \wedge
(\overline b \vee a) </tex>

Данная функция эквивалентна функции
<tex>
\overline a \to b \wedge
\overline b \to a \wedge
\overline a \to c \wedge
\overline c \to a \wedge
b \to c \wedge
\overline c \to \overline b \wedge
\overline a \to \overline b \wedge
a \to b
</tex>.

Построим ориентированный граф со следующими множествами вершинам и ребер:
множество вершин <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> имеют значение ноль.

 Ответ: <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 \wedge
c \to \overline a \wedge
a \to \overline c \wedge
\overline a \to b \wedge
\overline b \to a \wedge
b \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>.

Следовательно по ранее доказанной теореме, у данной функции решений нет.

 Ответ: Решений нет.

== Использование 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 :: Задача 2SAT (2-CNF) ]
*[https://en.wikipedia.org/wiki/2-satisfiability 2-satisfiability — Википедия]

[[Категория: Дискретная математика и алгоритмы]]

[[Категория: Булевы функции ]]

2SAT

2016-01-18T16:49:28Z

GARiK Carrot: /* Второй пример */ Исправлен tex

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

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

Рассмотрим любой дизъюнкт функции: <tex> a \vee b </tex>.
Несложно заметить, что это равнозначно записи <tex>(\overline a \to b \wedge b \to \overline a) </tex>.

Построим [[Основные_определения_теории_графов|ориентированный граф]], где вершинами будут аргументы и их отрицание, а ребрами будут ребра вида: <tex>\overline a \to b </tex> и <tex> b \to \overline a </tex> для каждого дизъюнкта функции <tex> a \vee b </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 x \to \overline x) </tex>.
|proof=
<tex>(\Rightarrow)</tex>Докажем достаточность: Пусть <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 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> одновременно. Докажем, что этого достаточно, чтобы <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>. Противоречие.
}}

Теперь мы можем собрать весь алгоритм воедино:

#Построим граф импликаций.
#Найдём в этом графе [[Отношение_связности,_компоненты_связности#Сильная связность | компоненты сильной связности]] за время <tex>O(N + M)</tex>, где <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>. Если это условие не выполняется, то вернуть "решение не существует".
#Если <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>.

== Примеры решения 2SAT ==
=== Первый пример ===

Рассмотрим следующую функцию: <tex> (a \vee b) \wedge
(a \vee c) \wedge
(\overline b \vee c) \wedge
(\overline b \vee a) </tex>

Данная функция эквивалентна функции
<tex>
\overline a \to b \wedge
\overline b \to a \wedge
\overline a \to c \wedge
\overline c \to a \wedge
b \to c \wedge
\overline c \to \overline b \wedge
\overline a \to \overline b \wedge
a \to b
</tex>.

Построим ориентированный граф со следующими множествами вершинам и ребер:
множество вершин <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> имеют значение ноль.

 Ответ: <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 \wedge
c \to \overline a \wedge
a \to \overline c \wedge
\overline a \to b \wedge
\overline b \to a \wedge
b \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>.

Следовательно по ранее доказанной теореме, у данной функции решений нет.

 Ответ: Решений нет.

== Использование 2SAT ==

Решение <tex>\mathrm {2SAT}</tex> может потребоваться в следующих задачах:
*латинские квадраты,
*квазигруппы,
*числа Рамсея,
*система Штейнера,
*проектирование протоколов (пример: для сетевых коммуникаций),
*электронная коммерция (Электронные аукционы и автоматизированные брокеры,
*теории кодирования, криптографии,
*проектирование и тестирование лекарств (мед. препаратов).

== См. также ==

*[[3CNFSAT | NP-полнота задачи о выполнимости булевой формулы в форме 3-КНФ]]

== Примечания ==

*[https://ru.wikipedia.org/wiki/Латинский_квадрат Латинские квадраты]
*[https://ru.wikipedia.org/wiki/Квазигруппа_(социология) Квазигруппы]
*[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 Числа Рамсея]
*[https://ru.wikipedia.org/wiki/Система_Штейнера Система Штейнера]

== Источники информации ==

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

[[Категория: Дискретная математика и алгоритмы]]

[[Категория: Булевы функции ]]

2SAT

2016-01-18T16:46:23Z

GARiK Carrot: Изменен порядок последних трех разделов.

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

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

Рассмотрим любой дизъюнкт функции: <tex> a \vee b </tex>.
Несложно заметить, что это равнозначно записи <tex>(\overline a \to b \wedge b \to \overline a) </tex>.

Построим [[Основные_определения_теории_графов|ориентированный граф]], где вершинами будут аргументы и их отрицание, а ребрами будут ребра вида: <tex>\overline a \to b </tex> и <tex> b \to \overline a </tex> для каждого дизъюнкта функции <tex> a \vee b </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 x \to \overline x) </tex>.
|proof=
<tex>(\Rightarrow)</tex>Докажем достаточность: Пусть <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 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> одновременно. Докажем, что этого достаточно, чтобы <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>. Противоречие.
}}

Теперь мы можем собрать весь алгоритм воедино:

#Построим граф импликаций.
#Найдём в этом графе [[Отношение_связности,_компоненты_связности#Сильная связность | компоненты сильной связности]] за время <tex>O(N + M)</tex>, где <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>. Если это условие не выполняется, то вернуть "решение не существует".
#Если <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>.

== Примеры решения 2SAT ==
=== Первый пример ===

Рассмотрим следующую функцию: <tex> (a \vee b) \wedge
(a \vee c) \wedge
(\overline b \vee c) \wedge
(\overline b \vee a) </tex>

Данная функция эквивалентна функции
<tex>
\overline a \to b \wedge
\overline b \to a \wedge
\overline a \to c \wedge
\overline c \to a \wedge
b \to c \wedge
\overline c \to \overline b \wedge
\overline a \to \overline b \wedge
a \to b
</tex>.

Построим ориентированный граф со следующими множествами вершинам и ребер:
множество вершин <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> имеют значение ноль.

 Ответ: <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 \wedge
c \to \overline a \wedge
a \to \overline c \wedge
\overline a \to b \wedge
\overline b \to a \wedge
b \to a \wedge
\overline b \to \overline a
</tex>

Построим ориентированный граф со следующими множествами вершинам и ребер:
множество вершин V = \{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>.

Следовательно по ранее доказанной теореме, у данной функции решений нет.

 Ответ: Решений нет.

== Использование 2SAT ==

Решение <tex>\mathrm {2SAT}</tex> может потребоваться в следующих задачах:
*латинские квадраты,
*квазигруппы,
*числа Рамсея,
*система Штейнера,
*проектирование протоколов (пример: для сетевых коммуникаций),
*электронная коммерция (Электронные аукционы и автоматизированные брокеры,
*теории кодирования, криптографии,
*проектирование и тестирование лекарств (мед. препаратов).

== См. также ==

*[[3CNFSAT | NP-полнота задачи о выполнимости булевой формулы в форме 3-КНФ]]

== Примечания ==

*[https://ru.wikipedia.org/wiki/Латинский_квадрат Латинские квадраты]
*[https://ru.wikipedia.org/wiki/Квазигруппа_(социология) Квазигруппы]
*[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 Числа Рамсея]
*[https://ru.wikipedia.org/wiki/Система_Штейнера Система Штейнера]

== Источники информации ==

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

[[Категория: Дискретная математика и алгоритмы]]

[[Категория: Булевы функции ]]

2SAT

2016-01-18T16:45:09Z

GARiK Carrot:

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

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

Рассмотрим любой дизъюнкт функции: <tex> a \vee b </tex>.
Несложно заметить, что это равнозначно записи <tex>(\overline a \to b \wedge b \to \overline a) </tex>.

Построим [[Основные_определения_теории_графов|ориентированный граф]], где вершинами будут аргументы и их отрицание, а ребрами будут ребра вида: <tex>\overline a \to b </tex> и <tex> b \to \overline a </tex> для каждого дизъюнкта функции <tex> a \vee b </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 x \to \overline x) </tex>.
|proof=
<tex>(\Rightarrow)</tex>Докажем достаточность: Пусть <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 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> одновременно. Докажем, что этого достаточно, чтобы <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>. Противоречие.
}}

Теперь мы можем собрать весь алгоритм воедино:

#Построим граф импликаций.
#Найдём в этом графе [[Отношение_связности,_компоненты_связности#Сильная связность | компоненты сильной связности]] за время <tex>O(N + M)</tex>, где <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>. Если это условие не выполняется, то вернуть "решение не существует".
#Если <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>.

== Примеры решения 2SAT ==
=== Первый пример ===

Рассмотрим следующую функцию: <tex> (a \vee b) \wedge
(a \vee c) \wedge
(\overline b \vee c) \wedge
(\overline b \vee a) </tex>

Данная функция эквивалентна функции
<tex>
\overline a \to b \wedge
\overline b \to a \wedge
\overline a \to c \wedge
\overline c \to a \wedge
b \to c \wedge
\overline c \to \overline b \wedge
\overline a \to \overline b \wedge
a \to b
</tex>.

Построим ориентированный граф со следующими множествами вершинам и ребер:
множество вершин <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> имеют значение ноль.

 Ответ: <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 \wedge
c \to \overline a \wedge
a \to \overline c \wedge
\overline a \to b \wedge
\overline b \to a \wedge
b \to a \wedge
\overline b \to \overline a
</tex>

Построим ориентированный граф со следующими множествами вершинам и ребер:
множество вершин V = \{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>.

Следовательно по ранее доказанной теореме, у данной функции решений нет.

 Ответ: Решений нет.

== Использование 2SAT ==

Решение <tex>\mathrm {2SAT}</tex> может потребоваться в следующих задачах:
*латинские квадраты,
*квазигруппы,
*числа Рамсея,
*система Штейнера,
*проектирование протоколов (пример: для сетевых коммуникаций),
*электронная коммерция (Электронные аукционы и автоматизированные брокеры,
*теории кодирования, криптографии,
*проектирование и тестирование лекарств (мед. препаратов).

== Примечания ==

*[https://ru.wikipedia.org/wiki/Латинский_квадрат Латинские квадраты]
*[https://ru.wikipedia.org/wiki/Квазигруппа_(социология) Квазигруппы]
*[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 Числа Рамсея]
*[https://ru.wikipedia.org/wiki/Система_Штейнера Система Штейнера]

== См. также ==

*[[3CNFSAT | NP-полнота задачи о выполнимости булевой формулы в форме 3-КНФ]]

== Источники информации ==

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

[[Категория: Дискретная математика и алгоритмы]]

[[Категория: Булевы функции ]]

2SAT

2016-01-18T16:25:38Z

GARiK Carrot:

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

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

Рассмотрим любой дизъюнкт функции: <tex> a \vee b </tex>.
Несложно заметить, что это равнозначно записи <tex>(\overline a \to b \wedge b \to \overline a) </tex>.

Построим [[Основные_определения_теории_графов|ориентированный граф]], где вершинами будут аргументы и их отрицание, а ребрами будут ребра вида: <tex>\overline a \to b </tex> и <tex> b \to \overline a </tex> для каждого дизъюнкта функции <tex> a \vee b </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 x \to \overline x) </tex>.
|proof=
<tex>(\Rightarrow)</tex>Докажем достаточность: Пусть <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 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> одновременно. Докажем, что этого достаточно, чтобы <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>. Противоречие.
}}

Теперь мы можем собрать весь алгоритм воедино:

#Построим граф импликаций.
#Найдём в этом графе [[Отношение_связности,_компоненты_связности#Сильная связность | компоненты сильной связности]] за время <tex>O(N + M)</tex>, где <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>. Если это условие не выполняется, то вернуть "решение не существует".
#Если <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>.

== Примеры решения 2SAT ==
=== Первый пример ===

Рассмотрим следующую функцию: <tex> (a \vee b) \wedge
(a \vee c) \wedge
(\overline b \vee c) \wedge
(\overline b \vee a) </tex>

Данная функция эквивалентна функции
<tex>
\overline a \to b \wedge
\overline b \to a \wedge
\overline a \to c \wedge
\overline c \to a \wedge
b \to c \wedge
\overline c \to \overline b \wedge
\overline a \to \overline b \wedge
a \to b
</tex>.

Построим ориентированный граф со следующими множествами вершинам и ребер:
множество вершин <tex> V = \{a, b, 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> имеют значение ноль.

 Ответ: <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 \wedge
c \to \overline a \wedge
a \to \overline c \wedge
\overline a \to b \wedge
\overline b \to a \wedge
b \to a \wedge
\overline b \to \overline a
</tex>

Построим ориентированный граф со следующими множествами вершинам и ребер:
множество вершин <tex> V = \{a, b, 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>.

Следовательно по ранее доказанной теореме, у данной функции решений нет.

 Ответ: Решений нет.

== Использование 2SAT ==

Решение 2SAT может потребоваться в следующих задачах:
*латинские квадраты,
*квазигруппы,
*числа Рамсея,
*система Штейнера,
*проектирование протоколов (пример: для сетевых коммуникаций),
*электронная коммерция (Электронные аукционы и автоматизированные брокеры,
*теории кодирования, криптографии,
*проектирование и тестирование лекарств (мед. препаратов).

== Примечания ==

*[https://ru.wikipedia.org/wiki/Латинский_квадрат Латинские квадраты]
*[https://ru.wikipedia.org/wiki/Квазигруппа_(социология) Квазигруппы]
*[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 Числа Рамсея]
*[https://ru.wikipedia.org/wiki/Система_Штейнера Система Штейнера]

== См. также ==

*[[3CNFSAT | NP-полнота задачи о выполнимости булевой формулы в форме 3-КНФ]]

== Источники информации ==

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

[[Категория: Дискретная математика и алгоритмы]]

[[Категория: Булевы функции ]]

2SAT

2016-01-18T16:03:51Z

GARiK Carrot: переименовал 2-SAT в 2SAT

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

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

Рассмотрим любой дизъюнкт функции: <tex> a \vee b </tex>.
Несложно заметить, что это равнозначно записи <tex>(\overline a \to b \wedge b \to \overline a) </tex>.

Построим [[Основные_определения_теории_графов|ориентированный граф]], где вершинами будут аргументы и их отрицание, а ребрами будут ребра вида: <tex>\overline a \to b </tex> и <tex> b \to \overline a </tex> для каждого дизъюнкта функции <tex> a \vee b </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 x \to \overline x) </tex>.
|proof=
<tex>(\Rightarrow)</tex>Докажем достаточность: Пусть <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 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> одновременно. Докажем, что этого достаточно, чтобы <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>. Противоречие.
}}

Теперь мы можем собрать весь алгоритм воедино:

#Построим граф импликаций.
#Найдём в этом графе [[Отношение_связности,_компоненты_связности#Сильная связность | компоненты сильной связности]] за время <tex>O(N + M)</tex>, где <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>. Если это условие не выполняется, то вернуть "решение не существует".
#Если <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 ==
=== Первый пример ===

Рассмотрим следующую функцию: <tex> (a \vee b) \wedge
(a \vee c) \wedge
(\overline b \vee c) \wedge
(\overline b \vee a) </tex>

Данная функция эквивалентна функции
<tex>
\overline a \to b \wedge
\overline b \to a \wedge
\overline a \to c \wedge
\overline c \to a \wedge
b \to c \wedge
\overline c \to \overline b \wedge
\overline a \to \overline b \wedge
a \to 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> имеют значение ноль

 Ответ: <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 \wedge
c \to \overline a \wedge
a \to \overline c \wedge
\overline a \to b \wedge
\overline b \to a \wedge
b \to a \wedge
\overline b \to \overline a
</tex>

Заметим следующий путь: <tex> a \to c \to \overline a \to b \to a </tex>

Отсюда следует, что <tex> a \to \overline a \to a </tex>

Следовательно по ранее доказанной теореме, у данной функции решений нет

 Ответ: Решений нет

== Использование 2-SAT ==

*[https://ru.wikipedia.org/wiki/Латинский_квадрат Латинские квадраты]
*[https://ru.wikipedia.org/wiki/Квазигруппа_(социология) Квазигруппы]
*[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 Числа Рамсея]
*[https://ru.wikipedia.org/wiki/Система_Штейнера Система Штейнера]
*Проектирование протоколов (пример: для сетевых коммуникаций)
*Электронная коммерция (Электронные аукционы и автоматизированные брокеры
*Теории кодирования, криптографии
*Проектирование и тестирование лекарств (мед. препаратов)

== См. также ==

*[[3CNFSAT | NP-полнота задачи о выполнимости булевой формулы в форме 3-КНФ]]

== Источники информации ==

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

[[Категория: Дискретная математика и алгоритмы]]

[[Категория: Булевы функции ]]

2-SAT

2016-01-18T16:03:51Z

GARiK Carrot: переименовал 2-SAT в 2SAT

#перенаправление [[2SAT]]

2SAT

2016-01-18T16:03:35Z

GARiK Carrot: /* Алгоритм решения */

2SAT

2016-01-16T08:35:46Z

GARiK Carrot: Добавлены примеры решения 2-SAT

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

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

Рассмотрим любой дизъюнкт функции: <tex> a \vee b </tex>.
Несложно заметить, что это равнозначно записи <tex>(\overline a \to b \wedge b \to \overline a) </tex>.

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

{{Теорема
|statement=
Для того, чтобы данная задача 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>.
|proof=
<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.

Компоненты сильной связности найдем за <tex>O(N + M)</tex>, затем проверим каждую из <tex>N</tex> переменных за <tex>O(N)</tex>. Следовательно асимптотика <tex>O(N + M)</tex>

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

Рассмотрим следующую функцию: <tex> (a \vee b) \wedge
(a \vee c) \wedge
(\overline b \vee c) \wedge
(\overline b \vee a) </tex>

Данная функция эквивалентна функции
<tex>
\overline a \to b \wedge
\overline b \to a \wedge
\overline a \to c \wedge
\overline c \to a \wedge
b \to c \wedge
\overline c \to \overline b \wedge
\overline a \to \overline b \wedge
a \to 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> имеют значение ноль

 Ответ: <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 \wedge
c \to \overline a \wedge
a \to \overline c \wedge
\overline a \to b \wedge
\overline b \to a \wedge
b \to a \wedge
\overline b \to \overline a
</tex>

Заметим следующий путь: <tex> a \to c \to \overline a \to b \to a </tex>

Отсюда следует, что <tex> a \to \overline a \to a </tex>

Следовательно по ранее доказанной теореме, у данной функции решений нет

 Ответ: Решений нет

== Использование 2-SAT ==

*[https://ru.wikipedia.org/wiki/Латинский_квадрат Латинские квадраты]
*[https://ru.wikipedia.org/wiki/Квазигруппа_(социология) Квазигруппы]
*[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 Числа Рамсея]
*[https://ru.wikipedia.org/wiki/Система_Штейнера Система Штейнера]
*Проектирование протоколов (пример: для сетевых коммуникаций)
*Электронная коммерция (Электронные аукционы и автоматизированные брокеры
*Теории кодирования, криптографии
*Проектирование и тестирование лекарств (мед. препаратов)

== См. также ==

*[[3CNFSAT | NP-полнота задачи о выполнимости булевой формулы в форме 3-КНФ]]

== Источники информации ==

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

[[Категория: Дискретная математика и алгоритмы]]

[[Категория: Булевы функции ]]

2SAT

2016-01-16T07:45:30Z

GARiK Carrot: Добавлено использование 2-SAT

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

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

Рассмотрим любой дизъюнкт функции: <tex> a \vee b </tex>.
Несложно заметить, что это равнозначно записи <tex>(\overline a \to b \wedge b \to \overline a) </tex>.

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

{{Теорема
|statement=
Для того, чтобы данная задача 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>.
|proof=
<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.

Компоненты сильной связности найдем за <tex>O(N + M)</tex>, затем проверим каждую из <tex>N</tex> переменных за <tex>O(N)</tex>. Следовательно асимптотика <tex>O(N + M)</tex>

== Использование 2-SAT ==

*[https://ru.wikipedia.org/wiki/Латинский_квадрат Латинские квадраты]
*[https://ru.wikipedia.org/wiki/Квазигруппа_(социология) Квазигруппы]
*[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 Числа Рамсея]
*[https://ru.wikipedia.org/wiki/Система_Штейнера Система Штейнера]
*Проектирование протоколов (пример: для сетевых коммуникаций)
*Электронная коммерция (Электронные аукционы и автоматизированные брокеры
*Теории кодирования, криптографии
*Проектирование и тестирование лекарств (мед. препаратов)

== См. также ==

*[[3CNFSAT | NP-полнота задачи о выполнимости булевой формулы в форме 3-КНФ]]

== Источники информации ==

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

[[Категория: Дискретная математика и алгоритмы]]

[[Категория: Булевы функции ]]

2SAT

2015-12-10T10:33:24Z

GARiK Carrot: Временно убран пример. Исправлено вступление, алгоритм решения

2SAT

2015-12-09T15:39:08Z

GARiK Carrot: /* Применение 2-SAT задач */ Добавлен пример применения 2-SAT

Рассмотрим функцию, записанную в виде 2-КНФ (КНФ Крома).

Решим задачу 2-SAT выполнимости данной функции.
{{Задача
|definition = 2-SAT (2-satisfiability) выполнимость данной функции — задача распределения аргументов таким образом, чтобы результат данной функции был равен <tex> 1 </tex>.
}}

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

Рассмотрим любой дизъюнкт функции: <tex> a \vee b </tex>.
Несложно заметить, что это равнозначно записи <tex>(\overline a \to b \wedge b \to \overline a) </tex>.

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

{{Теорема
|statement=
Для того, чтобы данная задача 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>.
|proof=
*Докажем достаточность: Пусть 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> 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>. Противоречие.
}}

Теперь мы можем собрать весь алгоритм воедино:

*Построим граф импликаций.
*Найдём в этом графе компоненты сильной связности за время <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 </tex>. Тогда пять из шестнадцати ограничений исчезнут, и останутся только 22 из импликаций.
Такое решение будет иметь циклы наподобие <tex> z \to \overline u \to x \to z </tex> или <tex> t \to \overline z \to t </tex>.
Можно заметить что значение <tex> tuwxyz = 110000 </tex> выполняют каждый дизъюнкт. Эти значения дают нам расписание, которое выполняет шесть из семи исходных условий, начиная с выступления (Tomlin, Unwin, Zany, Williams, Xie) в первый день в (Aladdin, Bellagio, Caesars, Desert, Excalibur).

== См. также ==

*[[КНФ | КНФ]]
*[[Специальные_формы_КНФ | Специальные формы КНФ. КНФ в форме Крона (2-КНФ)]]
*[[Основные_определения_теории_графов#.D0.9E.D1.80.D0.B8.D0.B5.D0.BD.D1.82.D0.B8.D1.80.D0.BE.D0.B2.D0.B0.D0.BD.D0.BD.D1.8B.D0.B5_.D0.B3.D1.80.D0.B0.D1.84.D1.8B | Ориентированные графы]]
*[[3CNFSAT | NP-полнота задачи о выполнимости булевой формулы в форме 3-КНФ]]
*[http://e-maxx.ru/algo/strong_connected_components MAXimal :: algo :: Поиск компонент сильной связности за O(N + M)]

== Источники информации ==

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

[[Категория: Дискретная математика и алгоритмы]]

[[Категория: Булевы функции ]]

2SAT

2015-12-09T09:41:47Z

GARiK Carrot: /* Алгоритм Решения */

2SAT

2015-12-03T19:14:27Z

GARiK Carrot: Добавлена расшифровка

2SAT

2015-12-03T17:53:11Z

GARiK Carrot: Добавлен алгоритм. Заменено "Определение" на "Задачу"

Рассмотрим функцию, записанную в виде 2-КНФ (КНФ Крома).

Решим задачу 2-SAT выполнимости данной функции.
{{Задача
|definition = 2-SAT выполнимость данной функции — задача распределения аргументов таким образом, чтобы результат данной функции был равен <tex> 1 </tex>.
}}

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

Рассмотрим любой дизъюнкт функции: <tex> a \vee b </tex>.
Несложно заметить, что это равнозначно записи <tex>(\overline a \to b \wedge b \to \overline a) </tex>.

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

{{Теорема
|statement=
Для того, чтобы данная задача 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>.
|proof=
*Докажем достаточность: Пусть 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> 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>. Противоречие.
}}

Теперь мы можем собрать весь алгоритм воедино:

*Построим граф импликаций.
*Найдём в этом графе компоненты сильной связности за время <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 задач ==

Алгоритм для решения 2-SAT может быть применим во всех задачах, где есть набор величин, каждая из которых может принимать 2 возможных значения, и есть связи между этими величинами:

* Расположение текстовых меток на карте или диаграмме. Имеется в виду нахождение такого расположения меток, при котором никакие две не пересекаются. Стоит заметить, что в общем случае, когда каждая метка может занимать множество различных позиций, мы получаем задачу general satisfiability, которая является NP-полной. Однако, если ограничиться только двумя возможными позициями, то полученная задача будет задачей 2-SAT.
* Расположение рёбер при рисовании графа. Аналогично предыдущему пункту, если ограничиться только двумя возможными способами провести ребро, то мы придём к 2-SAT.
* Составление расписания игр. Имеется в виду такая система, когда каждая команда должна сыграть с каждой по одному разу, а требуется распределить игры по типу домашняя-выездная, с некоторыми наложенными ограничениями.

== См. также ==

*[[КНФ | КНФ]]
*[[Специальные_формы_КНФ | Специальные формы КНФ. КНФ в форме Крона (2-КНФ)]]
*[[Основные_определения_теории_графов#.D0.9E.D1.80.D0.B8.D0.B5.D0.BD.D1.82.D0.B8.D1.80.D0.BE.D0.B2.D0.B0.D0.BD.D0.BD.D1.8B.D0.B5_.D0.B3.D1.80.D0.B0.D1.84.D1.8B | Ориентированные графы]]
*[[3CNFSAT | NP-полнота задачи о выполнимости булевой формулы в форме 3-КНФ]]
*[http://e-maxx.ru/algo/strong_connected_components MAXimal :: algo :: Поиск компонент сильной связности за O(N + M)]

== Источники информации ==

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

[[Категория: Дискретная математика и алгоритмы]]

[[Категория: Булевы функции ]]

2SAT

2015-12-03T17:15:36Z

GARiK Carrot: /* См. также */ Переделано в интервики

Рассмотрим функцию, записанную в виде 2-КНФ (КНФ Крома).

{{Определение
|definition =
2-SAT выполнимость данной функции — эта задача распределения аргументов таким образом, чтобы результат данной функции был равен 1.
}}

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

Рассмотрим любой дизъюнкт функции: <tex> a \vee b </tex> 
Несложно заметить, что это равнозначно записи <tex>(\overline a \to b \wedge b \to \overline a) </tex> 

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

{{Теорема
|statement=
Для того, чтобы данная задача 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>
|proof=
Пусть 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> должен быть равен 1. С другой стороны для того, чтобы из <tex> x </tex> достичь <tex> \overline x </tex> <tex> (\overline x \to x </tex> было верным), <tex> x </tex> должен быть равен 0. Отсюда следует противоречие. 

Пусть для любой переменной <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>. Противоречие.
}}

== Применение 2-SAT задач ==

Алгоритм для решения 2-SAT может быть применим во всех задачах, где есть набор величин, каждая из которых может принимать 2 возможных значения, и есть связи между этими величинами:

* Расположение текстовых меток на карте или диаграмме. Имеется в виду нахождение такого расположения меток, при котором никакие две не пересекаются. Стоит заметить, что в общем случае, когда каждая метка может занимать множество различных позиций, мы получаем задачу general satisfiability, которая является NP-полной. Однако, если ограничиться только двумя возможными позициями, то полученная задача будет задачей 2-SAT.
* Расположение рёбер при рисовании графа. Аналогично предыдущему пункту, если ограничиться только двумя возможными способами провести ребро, то мы придём к 2-SAT.
* Составление расписания игр. Имеется в виду такая система, когда каждая команда должна сыграть с каждой по одному разу, а требуется распределить игры по типу домашняя-выездная, с некоторыми наложенными ограничениями.

== См. также ==

*[[КНФ | КНФ]]
*[[Специальные_формы_КНФ | Специальные формы КНФ. КНФ в форме Крона (2-КНФ)]]
*[[Основные_определения_теории_графов#.D0.9E.D1.80.D0.B8.D0.B5.D0.BD.D1.82.D0.B8.D1.80.D0.BE.D0.B2.D0.B0.D0.BD.D0.BD.D1.8B.D0.B5_.D0.B3.D1.80.D0.B0.D1.84.D1.8B | Ориентированные графы]]
*[[3CNFSAT | NP-полнота задачи о выполнимости булевой формулы в форме 3-КНФ]]

== Источники информации ==

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

[[Категория: Дискретная математика и алгоритмы]]

[[Категория: Булевы функции ]]

2SAT

2015-12-03T17:13:55Z

GARiK Carrot: /* Источники информации */ Добавлена википедия

Рассмотрим функцию, записанную в виде 2-КНФ (КНФ Крома).

{{Определение
|definition =
2-SAT выполнимость данной функции — эта задача распределения аргументов таким образом, чтобы результат данной функции был равен 1.
}}

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

Рассмотрим любой дизъюнкт функции: <tex> a \vee b </tex> 
Несложно заметить, что это равнозначно записи <tex>(\overline a \to b \wedge b \to \overline a) </tex> 

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

{{Теорема
|statement=
Для того, чтобы данная задача 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>
|proof=
Пусть 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> должен быть равен 1. С другой стороны для того, чтобы из <tex> x </tex> достичь <tex> \overline x </tex> <tex> (\overline x \to x </tex> было верным), <tex> x </tex> должен быть равен 0. Отсюда следует противоречие. 

Пусть для любой переменной <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>. Противоречие.
}}

== Применение 2-SAT задач ==

Алгоритм для решения 2-SAT может быть применим во всех задачах, где есть набор величин, каждая из которых может принимать 2 возможных значения, и есть связи между этими величинами:

* Расположение текстовых меток на карте или диаграмме. Имеется в виду нахождение такого расположения меток, при котором никакие две не пересекаются. Стоит заметить, что в общем случае, когда каждая метка может занимать множество различных позиций, мы получаем задачу general satisfiability, которая является NP-полной. Однако, если ограничиться только двумя возможными позициями, то полученная задача будет задачей 2-SAT.
* Расположение рёбер при рисовании графа. Аналогично предыдущему пункту, если ограничиться только двумя возможными способами провести ребро, то мы придём к 2-SAT.
* Составление расписания игр. Имеется в виду такая система, когда каждая команда должна сыграть с каждой по одному разу, а требуется распределить игры по типу домашняя-выездная, с некоторыми наложенными ограничениями.

== См. также ==

*[http://neerc.ifmo.ru/wiki/index.php?title=КНФ - КНФ]
*[http://neerc.ifmo.ru/wiki/index.php?title=Специальные_формы_КНФ - Специальные формы КНФ. КНФ в форме Крона (2-КНФ)]
*[http://neerc.ifmo.ru/wiki/index.php?title=Основные_определения_теории_графов#.D0.9E.D1.80.D0.B8.D0.B5.D0.BD.D1.82.D0.B8.D1.80.D0.BE.D0.B2.D0.B0.D0.BD.D0.BD.D1.8B.D0.B5_.D0.B3.D1.80.D0.B0.D1.84.D1.8B - Ориентированные графы]
*[http://neerc.ifmo.ru/wiki/index.php?title=3CNFSAT - NP-полнота задачи о выполнимости булевой формулы в форме 3-КНФ]
== Источники информации ==

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

[[Категория: Дискретная математика и алгоритмы]]

[[Категория: Булевы функции ]]

2SAT

2015-12-02T09:43:49Z

GARiK Carrot: Добавлены категории

Рассмотрим функцию, записанную в виде 2-КНФ (КНФ Крома).

{{Определение
|definition =
2-SAT выполнимость данной функции — эта задача распределения аргументов таким образом, чтобы результат данной функции был равен 1.
}}

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

Рассмотрим любой дизъюнкт функции: <tex> a \vee b </tex> 
Несложно заметить, что это равнозначно записи <tex>(\overline a \to b \wedge b \to \overline a) </tex> 

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

{{Теорема
|statement=
Для того, чтобы данная задача 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>
|proof=
Пусть 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> должен быть равен 1. С другой стороны для того, чтобы из <tex> x </tex> достичь <tex> \overline x </tex> <tex> (\overline x \to x </tex> было верным), <tex> x </tex> должен быть равен 0. Отсюда следует противоречие. 

Пусть для любой переменной <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>. Противоречие.
}}

== Применение 2-SAT задач ==

Алгоритм для решения 2-SAT может быть применим во всех задачах, где есть набор величин, каждая из которых может принимать 2 возможных значения, и есть связи между этими величинами:

* Расположение текстовых меток на карте или диаграмме. Имеется в виду нахождение такого расположения меток, при котором никакие две не пересекаются. Стоит заметить, что в общем случае, когда каждая метка может занимать множество различных позиций, мы получаем задачу general satisfiability, которая является NP-полной. Однако, если ограничиться только двумя возможными позициями, то полученная задача будет задачей 2-SAT.
* Расположение рёбер при рисовании графа. Аналогично предыдущему пункту, если ограничиться только двумя возможными способами провести ребро, то мы придём к 2-SAT.
* Составление расписания игр. Имеется в виду такая система, когда каждая команда должна сыграть с каждой по одному разу, а требуется распределить игры по типу домашняя-выездная, с некоторыми наложенными ограничениями.

== См. также ==

*[http://neerc.ifmo.ru/wiki/index.php?title=КНФ - КНФ]
*[http://neerc.ifmo.ru/wiki/index.php?title=Специальные_формы_КНФ - Специальные формы КНФ. КНФ в форме Крона (2-КНФ)]
*[http://neerc.ifmo.ru/wiki/index.php?title=Основные_определения_теории_графов#.D0.9E.D1.80.D0.B8.D0.B5.D0.BD.D1.82.D0.B8.D1.80.D0.BE.D0.B2.D0.B0.D0.BD.D0.BD.D1.8B.D0.B5_.D0.B3.D1.80.D0.B0.D1.84.D1.8B - Ориентированные графы]
*[http://neerc.ifmo.ru/wiki/index.php?title=3CNFSAT - NP-полнота задачи о выполнимости булевой формулы в форме 3-КНФ]
== Источники информации ==

*[http://e-maxx.ru/algo/2_sat MAXimal :: algo :: Задача 2-SAT (2-CNF) ]

[[Категория: Дискретная математика и алгоритмы]]

[[Категория: Булевы функции ]]

2SAT

2015-12-02T07:53:27Z

GARiK Carrot: Добавлено применение 2-SAT. Добавлены новые ссылки

Рассмотрим функцию, записанную в виде 2-КНФ (КНФ Крома).

{{Определение
|definition =
2-SAT выполнимость данной функции — эта задача распределения аргументов таким образом, чтобы результат данной функции был равен 1.
}}

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

Рассмотрим любой дизъюнкт функции: <tex> a \vee b </tex> 
Несложно заметить, что это равнозначно записи <tex>(\overline a \to b \wedge b \to \overline a) </tex> 

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

{{Теорема
|statement=
Для того, чтобы данная задача 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>
|proof=
Пусть 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> должен быть равен 1. С другой стороны для того, чтобы из <tex> x </tex> достичь <tex> \overline x </tex> <tex> (\overline x \to x </tex> было верным), <tex> x </tex> должен быть равен 0. Отсюда следует противоречие. 

Пусть для любой переменной <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>. Противоречие.
}}

== Применение 2-SAT задач ==

Алгоритм для решения 2-SAT может быть применим во всех задачах, где есть набор величин, каждая из которых может принимать 2 возможных значения, и есть связи между этими величинами:

* Расположение текстовых меток на карте или диаграмме. Имеется в виду нахождение такого расположения меток, при котором никакие две не пересекаются. Стоит заметить, что в общем случае, когда каждая метка может занимать множество различных позиций, мы получаем задачу general satisfiability, которая является NP-полной. Однако, если ограничиться только двумя возможными позициями, то полученная задача будет задачей 2-SAT.
* Расположение рёбер при рисовании графа. Аналогично предыдущему пункту, если ограничиться только двумя возможными способами провести ребро, то мы придём к 2-SAT.
* Составление расписания игр. Имеется в виду такая система, когда каждая команда должна сыграть с каждой по одному разу, а требуется распределить игры по типу домашняя-выездная, с некоторыми наложенными ограничениями.

== См. также ==

*[http://neerc.ifmo.ru/wiki/index.php?title=КНФ - КНФ]
*[http://neerc.ifmo.ru/wiki/index.php?title=Специальные_формы_КНФ - Специальные формы КНФ. КНФ в форме Крона (2-КНФ)]
*[http://neerc.ifmo.ru/wiki/index.php?title=Основные_определения_теории_графов#.D0.9E.D1.80.D0.B8.D0.B5.D0.BD.D1.82.D0.B8.D1.80.D0.BE.D0.B2.D0.B0.D0.BD.D0.BD.D1.8B.D0.B5_.D0.B3.D1.80.D0.B0.D1.84.D1.8B - Ориентированные графы]
*[http://neerc.ifmo.ru/wiki/index.php?title=3CNFSAT - NP-полнота задачи о выполнимости булевой формулы в форме 3-КНФ]
== Источники информации ==

*[http://e-maxx.ru/algo/2_sat MAXimal :: algo :: Задача 2-SAT (2-CNF) ]

2SAT

2015-12-02T07:40:43Z

GARiK Carrot: Добавлен TEX. Добавлены ссылки на КНФ и 2-КНФ. Перенесено определение во вступление

2SAT

2015-11-30T16:45:04Z

GARiK Carrot: Новая страница: «== 2-SAT Выполнимость == Рассмотрим функцию, записанную в виде 2-КНФ (КНФ Крома). 2-SAT выполн...»

== 2-SAT Выполнимость ==

Рассмотрим функцию, записанную в виде 2-КНФ (КНФ Крома). 
2-SAT выполнимость данной функции - эта задача распределения аргументов таким образом, чтобы результат данной функции был равен 1.

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

Рассмотрим любой дизъюнкт функции: (a || b) 
Несложно заметить, что это равнозначно записи !a => b и !b => a 

Построим ориентированный граф, где вершинами будут аргументы и их отрицание, а ребрами будут ребра вида: !a => b и !b => a для каждого дизъюнкта функции (a || b) 

Для того, чтобы данная задача 2-SAT имела решение, необходимо и достаточно, чтобы для любой переменной x из вершины x нельзя достичь !x и из вершины !x нельзя достичь x одновременно. (!x => x && x => !x)

== Доказательство ==

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

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

== Ссылки ==

*[http://e-maxx.ru/algo/2_sat MAXimal :: algo :: Задача 2-SAT (2-CNF) ]

Обсуждение:Заглавная страница

2015-11-19T14:57:11Z

GARiK Carrot: переименовал Обсуждение:Заглавная страница в 2-SAT Выполнимость

Обсуждение:Заглавная страница

2015-11-19T14:53:58Z

GARiK Carrot:

Обсуждение:Заглавная страница

2015-11-18T10:44:44Z

GARiK Carrot: /* Доказательство */

* Будьте любезны, я не учился в вашем учреждении, подскажите: что значит "Непроверяемые конспекты" на заглавной странице? Дело в том, что на первый взгляд, очень интересен опубликованные конспекты по математическому анализу, но они "непроверяемы"? Это что значит? В них могут содержаться ошибки?
*: Именно это и значит. Данные конспекты пишут студенты, чтобы было проще готовиться к экзаменам. Они основаны на проводимых лекциях, сами студенты их перечитывают, но иногда в них могут содержаться случайные факты, ошибки, да и вообще они могут быть неполными. Хотя конспекты именно по математическому анализу достаточно хорошие. [[Участник:Shersh|Дмитрий Коваников]] 10:43, 4 мая 2015 (GST)

самая крутая заглавная страница в мире, ИМХО

'''Коллеги, пожалуйста, давайте без вандализма. Я понимаю, что первое апреля и хочется пошутить. Но шутки должны быть смешными и к месту.'''

* [http://inkscape.org/ http://inkscape.org/] — программа для рисования в векторе. Подходит для изображения графов, марковских цепей, схем из функциональных элементов и т.п. [[Участник:Rybak|Андрей Рыбак]] 23:01, 17 января 2011 (UTC)

* черт, на вики-конспектах какая-то проблема со временем. В комментариях показывает одно, в последних изменениях - другое.(сообщение написано в 4:42) --[[Участник:Dgerasimov|Дмитрий Герасимов]] 08:42, 12 июня 2011 (UTC)

* Кто сломал тег wikitex???111 --[[Участник:Dgerasimov|Дмитрий Герасимов]] 14:44, 10 октября 2011 (UTC)

* Кому вообще понадобились эти java-технологии? --[[Участник:Komarov|Андрей Комаров]] 00:43, 18 февраля 2012 (GST)
** Зря Андрей ты так про Джаву, зря-зря-зря... --[[Участник:Rybak|Андрей Рыбак]] 23:30, 29 февраля 2012 (GST)
** Это для первого курса 153N и второго 252N --[[Участник:Borisov|Borisov]] 02:04, 4 марта 2012 (GST)
** За год там ничего не появилось. Удалил. -- [[Участник:Dmitriy D.|Dmitriy D.]] 08:14, 9 января 2013 (GST)

== Ссылки на источники ==

* Почему бы не организовать ссылки на источники, как в Википедии? С тегом <nowiki><ref></ref></nowiki> --[[Участник:Rybak|Андрей Рыбак]] 20:13, 29 апреля 2012 (GST)

== Имена преподавателей ==

Андрей Сергеевич Станкевич

Федор Николаевич Царев

Корнеев Георгий Александрович

Что-то тут не так. Мне кстати последний вариант больше нравится.

== 2-SAT Выполнимость ==

Рассмотрим функцию, записанную в виде 2-КНФ (КНФ Крома). 
2-SAT выполнимость данной функции - эта задача распределения аргументов таким образом, чтобы результат данной функции был равен 1.

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

Рассмотрим любой дизъюнкт функции: (a || b) 
Несложно заметить, что это равнозначно записи !a => b и !b => a 

Построим ориентированный граф, где вершинами будут аргументы и их отрицание, а ребрами будут ребра вида: !a => b и !b => a для каждого дизъюнкта функции (a || b) 

Для того, чтобы данная задача 2-SAT имела решение, необходимо и достаточно, чтобы для любой переменной x из вершины x нельзя достичь !x и из вершины !x нельзя достичь x одновременно. (!x => x && x => !x)

== Доказательство ==

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

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

== Источники ==

MAXimal :: algo :: Задача 2-SAT (2-CNF) <ref> http://e-maxx.ru/algo/2_sat </ref>

Обсуждение:Заглавная страница

2015-11-18T10:41:35Z

GARiK Carrot: /* Алгоритм Решения */

Обсуждение:Заглавная страница

2015-11-18T10:40:43Z

GARiK Carrot: /* 2-SAT Выполнимость */ Новая тема

* Будьте любезны, я не учился в вашем учреждении, подскажите: что значит "Непроверяемые конспекты" на заглавной странице? Дело в том, что на первый взгляд, очень интересен опубликованные конспекты по математическому анализу, но они "непроверяемы"? Это что значит? В них могут содержаться ошибки?
*: Именно это и значит. Данные конспекты пишут студенты, чтобы было проще готовиться к экзаменам. Они основаны на проводимых лекциях, сами студенты их перечитывают, но иногда в них могут содержаться случайные факты, ошибки, да и вообще они могут быть неполными. Хотя конспекты именно по математическому анализу достаточно хорошие. [[Участник:Shersh|Дмитрий Коваников]] 10:43, 4 мая 2015 (GST)

самая крутая заглавная страница в мире, ИМХО

'''Коллеги, пожалуйста, давайте без вандализма. Я понимаю, что первое апреля и хочется пошутить. Но шутки должны быть смешными и к месту.'''

* [http://inkscape.org/ http://inkscape.org/] — программа для рисования в векторе. Подходит для изображения графов, марковских цепей, схем из функциональных элементов и т.п. [[Участник:Rybak|Андрей Рыбак]] 23:01, 17 января 2011 (UTC)

* черт, на вики-конспектах какая-то проблема со временем. В комментариях показывает одно, в последних изменениях - другое.(сообщение написано в 4:42) --[[Участник:Dgerasimov|Дмитрий Герасимов]] 08:42, 12 июня 2011 (UTC)

* Кто сломал тег wikitex???111 --[[Участник:Dgerasimov|Дмитрий Герасимов]] 14:44, 10 октября 2011 (UTC)

* Кому вообще понадобились эти java-технологии? --[[Участник:Komarov|Андрей Комаров]] 00:43, 18 февраля 2012 (GST)
** Зря Андрей ты так про Джаву, зря-зря-зря... --[[Участник:Rybak|Андрей Рыбак]] 23:30, 29 февраля 2012 (GST)
** Это для первого курса 153N и второго 252N --[[Участник:Borisov|Borisov]] 02:04, 4 марта 2012 (GST)
** За год там ничего не появилось. Удалил. -- [[Участник:Dmitriy D.|Dmitriy D.]] 08:14, 9 января 2013 (GST)

== Ссылки на источники ==

* Почему бы не организовать ссылки на источники, как в Википедии? С тегом <nowiki><ref></ref></nowiki> --[[Участник:Rybak|Андрей Рыбак]] 20:13, 29 апреля 2012 (GST)

== Имена преподавателей ==

Андрей Сергеевич Станкевич

Федор Николаевич Царев

Корнеев Георгий Александрович

Что-то тут не так. Мне кстати последний вариант больше нравится.

== 2-SAT Выполнимость ==

Рассмотрим функцию, записанную в виде 2-КНФ (КНФ Крома). 
2-SAT выполнимость данной функции - эта задача распределения аргументов таким образом, чтобы результат данной функции был равен 1.

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

Рассмотрим любой дизъюнкт функции: (a || b) 
Несложно заметить, что это равнозначно записи !a => b и !b => a 

Построим ориентированный граф, где вершинами будут аргументы и их отрицание, а ребрами будут ребра вида: !a => b и !b => a для каждого дизъюнкта функции (a || b) 

Для того, чтобы данная задача 2-SAT имела решение, необходимо и достаточно, чтобы для любой переменной x из вершины x нельзя достичь !x и из вершины !x нельзя достичь x одновременно. (!x => x && x => !x)

== Доказательство ==

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

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