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

Материал из Викиконспекты
Перейти к: навигация, поиск
(Временно убран пример. Исправлено вступление, алгоритм решения)
(Добавлено использование 2-SAT)
Строка 28: Строка 28:
  
 
Компоненты сильной связности найдем за <tex>O(N + M)</tex>, затем проверим каждую из <tex>N</tex> переменных за <tex>O(N)</tex>. Следовательно асимптотика <tex>O(N + M)</tex>
 
Компоненты сильной связности найдем за <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/Система_Штейнера Система Штейнера]
 +
*Проектирование протоколов (пример: для сетевых коммуникаций)
 +
*Электронная коммерция (Электронные аукционы и автоматизированные брокеры
 +
*Теории кодирования, криптографии
 +
*Проектирование и тестирование лекарств (мед. препаратов)
  
 
== См. также ==
 
== См. также ==

Версия 10:45, 16 января 2016

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


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

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

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

Теорема:
Для того, чтобы данная задача 2-SAT имела решение, необходимо и достаточно, чтобы для любой переменной [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]Докажем достаточность: Пусть 2-SAT имеет решение. Докажем, что не может быть такого, чтобы для любой переменной [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] (\overline x \to 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] одновременно. Докажем, что этого достаточно, чтобы 2-SAT имело решение. Пусть из [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]
  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], то переменной x выбираем значение true, иначе - false.

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

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

См. также

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