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

Материал из Викиконспекты
Перейти к: навигация, поиск
м (rollbackEdits.php mass rollback)
 
Строка 1: Строка 1:
{| class="wikitable" align="center" style="color: red; background-color: black; font-size: 56px; width: 800px;"
 
|+
 
|-align="center"
 
|'''НЕТ ВОЙНЕ'''
 
|-style="font-size: 16px;"
 
|
 
24 февраля 2022 года российское руководство во главе с Владимиром Путиным развязало агрессивную войну против Украины. В глазах всего мира это военное преступление совершено от лица всей страны, всех россиян.
 
 
Будучи гражданами Российской Федерации, мы против своей воли оказались ответственными за нарушение международного права, военное вторжение и массовую гибель людей. Чудовищность совершенного преступления не оставляет возможности промолчать или ограничиться пассивным несогласием.
 
 
Мы убеждены в абсолютной ценности человеческой жизни, в незыблемости прав и свобод личности. Режим Путина — угроза этим ценностям. Наша задача — обьединить все силы для сопротивления ей.
 
 
Эту войну начали не россияне, а обезумевший диктатор. И наш гражданский долг — сделать всё, чтобы её остановить.
 
 
''Антивоенный комитет России''
 
|-style="font-size: 16px;"
 
|Распространяйте правду о текущих событиях, оберегайте от пропаганды своих друзей и близких. Изменение общественного восприятия войны - ключ к её завершению.
 
|-style="font-size: 16px;"
 
|[https://meduza.io/ meduza.io], [https://www.youtube.com/c/popularpolitics/videos Популярная политика], [https://novayagazeta.ru/ Новая газета], [https://zona.media/ zona.media], [https://www.youtube.com/c/MackNack/videos Майкл Наки].
 
|}
 
 
 
{{Задача
 
{{Задача
 
|definition = <b><tex>\mathrm {2SAT}</tex></b> (2-satisfiability) выполнимость функции — задача распределения аргументов в булевой [[КНФ|КНФ]] функции, записанной в виде [[Специальные_формы_КНФ|2-КНФ (КНФ Крома)]], таким образом, чтобы результат данной функции был равен <tex> 1 </tex>.
 
|definition = <b><tex>\mathrm {2SAT}</tex></b> (2-satisfiability) выполнимость функции — задача распределения аргументов в булевой [[КНФ|КНФ]] функции, записанной в виде [[Специальные_формы_КНФ|2-КНФ (КНФ Крома)]], таким образом, чтобы результат данной функции был равен <tex> 1 </tex>.

Текущая версия на 19:29, 4 сентября 2022

Задача:
[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],
  • проектирование протоколов (пример: для сетевых коммуникаций),
  • электронная коммерция (Электронные аукционы и автоматизированные брокеры,
  • теории кодирования, криптографии,
  • проектирование и тестирование лекарств (мед. препаратов).

См. также

Примечания

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