2SAT — различия между версиями

Материал из Викиконспекты
Перейти к: навигация, поиск
(Добавлено применение 2-SAT. Добавлены новые ссылки)
м (Первый пример)
(Метки: правка с мобильного устройства, правка из мобильной версии)
(не показаны 24 промежуточные версии 4 участников)
Строка 1: Строка 1:
Рассмотрим функцию, записанную в виде 2-КНФ (КНФ Крома).
+
{{Задача
 
+
|definition = <b><tex>\mathrm {2SAT}</tex></b> (2-satisfiability) выполнимость функции — задача распределения аргументов в булевой [[КНФ|КНФ]] функции, записанной в виде [[Специальные_формы_КНФ|2-КНФ (КНФ Крома)]], таким образом, чтобы результат данной функции был равен <tex> 1 </tex>.
{{Определение
 
|definition =
 
2-SAT выполнимость данной функции — эта задача распределения аргументов таким образом, чтобы результат данной функции был равен 1.
 
 
}}
 
}}
  
 +
== Алгоритм решения ==
  
== Алгоритм Решения ==
 
  
 +
Рассмотрим любой дизъюнкт функции: <tex> a \vee b </tex>.
 +
Несложно заметить, что это равнозначно записи <tex>(\overline a \to b \wedge \overline b \to a) </tex>.
  
Рассмотрим любой дизъюнкт функции: <tex> a \vee b </tex> <br>
+
Построим [[Основные_определения_теории_графов|ориентированный граф]], где вершинами будут аргументы и их отрицание, а ребрами будут ребра вида: <tex>\overline a \to b </tex> и <tex> \overline b \to a </tex> для каждого дизъюнкта функции <tex> a \vee b </tex>.
Несложно заметить, что это равнозначно записи <tex>(\overline a \to b \wedge b \to \overline a) </tex> <br>
 
 
 
Построим ориентированный граф, где вершинами будут аргументы и их отрицание, а ребрами будут ребра вида: <tex>\overline a \to b </tex> и <tex> b \to \overline a </tex> для каждого дизъюнкта функции <tex> a \vee b </tex> <br>
 
  
 
{{Теорема
 
{{Теорема
 
|statement=
 
|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>
+
Для того, чтобы данная задача <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=
 
|proof=
Пусть 2-SAT имеет решение. <br>
+
<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> (x \to \overline x </tex> было верным), <tex> x </tex> должен быть равен 0. Отсюда следует противоречие.
Докажем, что не может быть такого, чтобы для любой переменной <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> <br>
 
Тогда чтобы из <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. Отсюда следует противоречие. <br> <br>
 
  
Пусть для любой переменной <tex> x </tex> из вершины <tex> x </tex> нельзя достичь <tex> \overline x </tex> и из вершины <tex> \overline x </tex> нельзя достичь <tex> x </tex> одновременно. <br>
+
<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>. Противоречие.
Докажем, что этого достаточно, чтобы 2-SAT имело решение. <br>
 
Пусть из <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>. <br>
 
Если из <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 задач ==
+
Теперь мы можем собрать весь алгоритм воедино:
 +
 
 +
#Построим граф импликаций.
 +
#<i>Найдём в этом графе [[Отношение_связности,_компоненты_связности#Сильная связность | компоненты сильной связности]] за время <tex>O(N + M)</tex></i>, где <tex> N </tex> — количество вершин в графе (удвоенное количество переменных), а <tex> M </tex> — количество ребер графа (удвоенное количество дизъюнктов).
 +
#Пусть <tex>comp[v]</tex> — это номер компоненты сильной связности, которой принадлежит вершине <tex>v</tex>. Проверим, что для каждой переменной <tex>x</tex> вершины <tex>x</tex> и <tex>\overline x</tex> лежат в разных компонентах, т.е. <tex>comp[x] \ne comp[\overline x]</tex>. Если это условие не выполняется, то вернуть <i>решение не существует</i>.
 +
#Если <tex>comp[x] > comp[\overline x]</tex>, то переменной <tex>x</tex> выбираем значение <tex> \mathtt {true}</tex>, иначе — <tex> \mathtt {false}</tex>.
 +
 
 +
Компоненты сильной связности найдем за <tex>O(N + M)</tex>, затем проверим каждую из <tex>N</tex> переменных за <tex>O(N)</tex>. Следовательно асимптотика <tex>O(N + M)</tex>.
 +
 
 +
== Примеры решения 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), (b, a)\}</tex>.
 +
 
 +
Рассмотрим в графе следующие пути:
 +
* <tex> \overline a \to b \to a </tex>
 +
* <tex> \overline a \to \overline b \to a </tex>
 +
* <tex> \overline c \to a </tex>
 +
* <tex> a \to c </tex>
 +
* <tex> \overline a \to b \to c </tex>.
 +
 
 +
Т.к. <tex> \overline a \to a </tex>, то <tex> a = 1, \overline a = 0 </tex>.
 +
 
 +
Т.к. <tex> a \to c </tex> и <tex> a = 1 </tex>, то <tex> c = 1, \overline c = 0 </tex>.
 +
 
 +
Значения <tex> b </tex> может быть любым, т.к. все вершины, из которых можно добраться в <tex> b </tex> имеют значение ноль.
 +
 
 +
<b> Ответ: </b> <tex> a = 1, b = 0, c = 1 </tex> или <tex> a = 1, b = 1, c = 1 </tex>.
 +
 
 +
=== Второй пример ===
 +
 
 +
Рассмотрим следующую функцию:
 +
<tex>
 +
(\overline a \vee c) \wedge
 +
(\overline c \vee \overline a) \wedge
 +
(a \vee b) \wedge
 +
(\overline b \vee a)
 +
</tex>
 +
 
 +
Данная функция эквивалентна функции
 +
<tex>
 +
a \to c \wedge
 +
\overline c \to \overline a \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>.
  
Алгоритм для решения 2-SAT может быть применим во всех задачах, где есть набор величин, каждая из которых может принимать 2 возможных значения, и есть связи между этими величинами:
+
Следовательно по ранее доказанной теореме, у данной функции решений нет.
  
* Расположение текстовых меток на карте или диаграмме. Имеется в виду нахождение такого расположения меток, при котором никакие две не пересекаются. Стоит заметить, что в общем случае, когда каждая метка может занимать множество различных позиций, мы получаем задачу general satisfiability, которая является NP-полной. Однако, если ограничиться только двумя возможными позициями, то полученная задача будет задачей 2-SAT.
+
<b> Ответ: </b> Решений нет.
* Расположение рёбер при рисовании графа. Аналогично предыдущему пункту, если ограничиться только двумя возможными способами провести ребро, то мы придём к 2-SAT.
 
* Составление расписания игр. Имеется в виду такая система, когда каждая команда должна сыграть с каждой по одному разу, а требуется распределить игры по типу домашняя-выездная, с некоторыми наложенными ограничениями.
 
  
 +
== Использование 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>,
 +
*проектирование протоколов (пример: для сетевых коммуникаций),
 +
*электронная коммерция (Электронные аукционы и автоматизированные брокеры,
 +
*теории кодирования, криптографии,
 +
*проектирование и тестирование лекарств (мед. препаратов).
  
 
== См. также ==
 
== См. также ==
  
*[http://neerc.ifmo.ru/wiki/index.php?title=КНФ - КНФ]
+
*[[3CNFSAT | NP-полнота задачи о выполнимости булевой формулы в форме 3-КНФ]]
*[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-КНФ]
+
<references/>
 +
 
 
== Источники информации ==
 
== Источники информации ==
  
*[http://e-maxx.ru/algo/2_sat MAXimal :: algo :: Задача 2-SAT (2-CNF) ]
+
*[http://e-maxx.ru/algo/2_sat MAXimal :: algo :: Задача 2SAT (2-CNF) ]
 +
*[https://en.wikipedia.org/wiki/2-satisfiability Википедия — 2-satisfiability]
 +
 
 +
[[Категория: Дискретная математика и алгоритмы]]
 +
 
 +
[[Категория: Булевы функции ]]

Версия 13:09, 22 октября 2019

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


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

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

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

Теорема:
Для того, чтобы данная задача [math]\mathrm {2SAT}[/math] имела решение, необходимо и достаточно, чтобы для любой переменной [math] x [/math] из вершины [math] x [/math] нельзя достичь [math] \overline x [/math] и из вершины [math] \overline x [/math] нельзя достичь [math] x [/math] одновременно. [math](\overline x \to x) \wedge (x \to \overline x) [/math].
Доказательство:
[math]\triangleright[/math]

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

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

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

  1. Построим граф импликаций.
  2. Найдём в этом графе компоненты сильной связности за время [math]O(N + M)[/math], где [math] N [/math] — количество вершин в графе (удвоенное количество переменных), а [math] M [/math] — количество ребер графа (удвоенное количество дизъюнктов).
  3. Пусть [math]comp[v][/math] — это номер компоненты сильной связности, которой принадлежит вершине [math]v[/math]. Проверим, что для каждой переменной [math]x[/math] вершины [math]x[/math] и [math]\overline x[/math] лежат в разных компонентах, т.е. [math]comp[x] \ne comp[\overline x][/math]. Если это условие не выполняется, то вернуть решение не существует.
  4. Если [math]comp[x] \gt comp[\overline x][/math], то переменной [math]x[/math] выбираем значение [math] \mathtt {true}[/math], иначе — [math] \mathtt {false}[/math].

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

Примеры решения 2SAT

Первый пример

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

Данная функция эквивалентна функции [math] \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 [/math].

Построим ориентированный граф со следующими множествами вершинам и ребер: множество вершин [math] V = \{a, b, c, \overline a, \overline b, \overline c\}, [/math] множество ребер [math] E = \{(\overline a, b), (\overline b, a), (\overline a, c), (\overline c, a), (b, c), (\overline c, \overline b), (\overline a, \overline b), (b, a)\}[/math].

Рассмотрим в графе следующие пути:

  • [math] \overline a \to b \to a [/math]
  • [math] \overline a \to \overline b \to a [/math]
  • [math] \overline c \to a [/math]
  • [math] a \to c [/math]
  • [math] \overline a \to b \to c [/math].

Т.к. [math] \overline a \to a [/math], то [math] a = 1, \overline a = 0 [/math].

Т.к. [math] a \to c [/math] и [math] a = 1 [/math], то [math] c = 1, \overline c = 0 [/math].

Значения [math] b [/math] может быть любым, т.к. все вершины, из которых можно добраться в [math] b [/math] имеют значение ноль.

Ответ: [math] a = 1, b = 0, c = 1 [/math] или [math] a = 1, b = 1, c = 1 [/math].

Второй пример

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

Данная функция эквивалентна функции [math] 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 [/math]

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

Заметим следующий путь: [math] a \to c \to \overline a \to b \to a [/math].

Отсюда следует, что [math] a \to \overline a \to a [/math].

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

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

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

Решение [math]\mathrm {2SAT}[/math] может потребоваться в следующих задачах:

  • латинские квадраты[1],
  • квазигруппы[2],
  • числа Рамсея[3],
  • система Штейнера[4],
  • проектирование протоколов (пример: для сетевых коммуникаций),
  • электронная коммерция (Электронные аукционы и автоматизированные брокеры,
  • теории кодирования, криптографии,
  • проектирование и тестирование лекарств (мед. препаратов).

См. также

Примечания

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