Изменения

Перейти к: навигация, поиск

XOR-SAT

14 113 байт добавлено, 17:43, 20 июня 2017
м
Источники информации
{{Задача
|definition = <b><tex>\mathrm {XORSAT}</tex></b> (англ. ''XOR-satisfiability'') выполнимость функции — задача распределения аргументов в булевой [[КНФ|КНФ]] функции, записанной в виде XOR-КНФ, таким образом, чтобы результат данной функции был равен <tex> 1 </tex>.
}}
== Описание ==
Одним из особых случаев <b><tex>\mathrm {SAT}</tex></b> является класс задач, где каждый конъюнкт содержит операции <tex>\oplus</tex> (т. е. исключающее или), а не (обычные) <tex>\lor</tex> операторы.(Формально, обобщенная КНФ с тернарным булевым оператором <tex> R </tex> работает только если <tex> 1 </tex> или <tex> 3 </tex> переменные дают <b><tex>\mathrm mathtt {TRUEtrue}</tex></b> в своих аргументах. Конъюнкты,имеющие более <tex> 3 </tex> переменных могут быть преобразованы в сочетании с формулой преобразования с сохранением выполнимости булевой функции(ссылка на книгу ниже), т. е. <b><tex>\mathrm {XOR}</tex></b>-<b><tex>\mathrm {SAT}</tex></b> может быть снижена до <b><tex>\mathrm {XOR}</tex></b>-<b><tex>\mathrm {3}</tex></b>-<b><tex>\mathrm {SAT}</tex></b>)<ref>''Alfred V. Aho; John E. Hopcroft; Jeffrey D. Ullman.''The Design and Analysis of Computer Algorithms. Addison-Wesley.; здесь: Thm.10.4,1974.</ref>
Это задача [[Класс P|<tex>\mathrm {P}</tex>-класса]], так как <tex>\mathrm {XOR}</tex>-<tex>\mathrm {SAT}</tex> формулу можно рассматривать как систему линейных уравнений по модулю <tex>2</tex>, которая, в свою очередь, может быть решена за <tex>O(n^3)</tex> методом Гаусса <ref>[https://ru.wikipedia.org/wiki/%D0%9C%D0%B5%D1%82%D0%BE%D0%B4_%D0%93%D0%B0%D1%83%D1%81%D1%81%D0%B0 Метод Гаусса]</ref>.Такое представление возможно на основе связи между Булевой алгеброй и Булевым [[Определение кольца, подкольца, изоморфизмы колец|кольцом]] <ref>[https://en.wikipedia.org/wiki/Boolean_algebra_(structure)#Boolean_rings Связь между Булевой алгеброй и Булевым кольцом]</ref> и том факте, что арифметика по модулю <tex>2</tex> образует конечное поле <ref>[https://ru.wikipedia.org/wiki/%D0%9A%D0%BE%D0%BD%D0%B5%D1%87%D0%BD%D0%BE%D0%B5_%D0%BF%D0%BE%D0%BB%D0%B5 Конечное поле ]</ref>.
Это задача [[Класс P|Р-класса]],так как ==Пример решения XORSAT=====Пример===<font color='red'>Красные пункты<b/font>могут быть добавлены для возможности представления КНФ-функции в виде <tex>\mathrm {XOR}</tex></b>-<b><tex>\mathrm {SAT}</tex></b> формулу можно рассматривать как систему линейных уравнений по модулю 2,которая ,в свою очередь, может быть решена за .{| class="wikitable"!<tex>O(n^3a \oplus b \oplus c) \land (b \oplus \neg c \oplus d) \land (a \oplus b \oplus \neg d) \land (a \oplus \neg b \oplus \neg c)</tex> методом Гаусса! style="background: #ffdddd;" |<reftex>12213|https://ru.wikipedia.org/wiki/%D0%9C%D0%B5%D1%82%D0%BE%D0%B4_%D0%93%D0%B0%D1%83%D1%81%D1%81%D0%B0><\ref>.Такое представление возможно на основе связи между Булевой алгеброй и Булевым кольцом <ref>https://en.wikipedia.org/wiki/Boolean_algebra_land (structure\neg a \oplus b \oplus c)#Boolean_rings</ref> и том факте,что арифметика по модулю 2 образует конечное поле <ref>https://ru.wikipedia.org/wiki/%D0%9A%D0%BE%D0%BD%D0%B5%D1%87%D0%BD%D0%BE%D0%B5_%D0%BF%D0%BE%D0%BB%D0%B5</reftex>.|}{| class="wikitable"|+!colspan="2"|Решение XOR-SAT задачи методом Гаусса|-align=="center"!
<center>
{| class="wikitable" align="center" style="color: blue; background-color:#ffffcc;" cellpadding="10"
|+
!colspan="52"|Система уравнений|-align="center"!("<tex>1</tex>" означает «истинно», "<tex>0</tex>" означает «ложно»)Каждый конъюнкт ведет к одному уравнению.|
|-align="center"
!Переменные
|! width="20%" | ЗначенияЗначение
|-align="center"
! <tex> a </tex> <tex>\oplus</tex> <tex> c </tex> <tex>\oplus</tex> <tex> d </tex>
|-align="center"
! style="background: #ffdddd;" |<tex> \neg a </tex> <tex>\oplus</tex> <tex> b </tex> <tex>\oplus</tex> <tex> c </tex>
! style="background: #ffdddd;" |<tex> =1 </tex>|}</center>!(«<tex>1</tex>» означает «<tex> \mathtt {true}</tex>», «<tex>0</tex>» означает «<tex> \mathtt {false}</tex>»)Каждый конъюнкт ведет к одному уравнению.|-align="center"!<center>{| class="wikitable" align="center" style="color: blue; background-color:#ffffcc;" cellpadding="10"|+!colspan="2"|Нормированная система уравнений|-align="center"!Переменные|! width="20%" | Значение|-align="center"! <tex> a </tex> <tex>\oplus</tex> <tex> c </tex> <tex>\oplus</tex> <tex> d </tex> |<tex>=1</tex>|-align="center"! <tex> b </tex> <tex>\oplus</tex> <tex> c </tex> <tex>\oplus</tex> <tex> d </tex> |<tex>=0</tex>|-align="center"! <tex> a </tex> <tex>\oplus</tex> <tex> b </tex> <tex>\oplus</tex> <tex> d </tex> |<tex>=0</tex>|-align="center"! <tex> a </tex> <tex>\oplus</tex> <tex> b </tex> <tex>\oplus</tex> <tex> c </tex> |<tex>=1</tex>|-align="center"! style="background: #ffdddd;" |<tex> a </tex> <tex>\oplus</tex> <tex> b </tex> <tex>\oplus</tex> <tex> c </tex>! style="background: #ffdddd;" |<tex> =0 </tex>|}</center>!Используя свойства Булевых [[Определение кольца, подкольца, изоморфизмы колец|колец]] (<tex>\neg x=1 \oplus x</tex>, <tex>x \oplus x=1</tex>),<br>избавимся от отрицаний в нашей системе|-align="center"!<center>{| class="wikitable" align="center" style="color: blue; background-color:#ffffcc;" cellpadding="10"|+!colspan="6"|Матрица соответствующих коэффициентов|-align="center" !class="dark"| <tex>a</tex> !class="dark"| <tex>b</tex> !class="dark"| <tex>c</tex> !class="dark"| <tex>d</tex> !class="green" style="font-weight:normal" style="background: #ddffdd;"||Строка|-align="center" !class="dark" style="font-weight:normal"| <tex>1</tex> !class="dark" style="font-weight:normal"| <tex>0</tex> !class="dark" style="font-weight:normal"| <tex>1</tex> !class="dark" style="font-weight:normal"| <tex>1</tex> !class="green" style="font-weight:normal" style="background: #ddffdd;"| <tex>1</tex>| <tex>A</tex>|-align="center" !class="dark" style="font-weight:normal"| <tex>0</tex> !class="dark" style="font-weight:normal"| <tex>1</tex> !class="dark" style="font-weight:normal"| <tex>1</tex> !class="dark" style="font-weight:normal"| <tex>1</tex> !class="green" style="font-weight:normal" style="background: #ddffdd;"| <tex>0</tex>| <tex>B</tex>|-align="center" !class="dark" style="font-weight:normal"| <tex>1</tex> !class="dark" style="font-weight:normal"| <tex>1</tex> !class="dark" style="font-weight:normal"| <tex>0</tex> !class="dark" style="font-weight:normal"| <tex>1</tex> !class="green" style="font-weight:normal" style="background: #ddffdd;"| <tex>0</tex>| <tex>C</tex>|-align="center" !class="dark" style="font-weight:normal"| <tex>1</tex> !class="dark" style="font-weight:normal"| <tex>1</tex> !class="dark" style="font-weight:normal"| <tex>1</tex> !class="dark" style="font-weight:normal"| <tex>0</tex> !class="green" style="font-weight:normal" style="background: #ddffdd;"| <tex>1</tex>| <tex>D</tex>|}</center>!Составим матрицу по следующему правилу:Если переменная присутствовала в данном конъюнкте<br>ставим в ячейку <tex>1</tex>, иначе <tex>0</tex>|-align="center"!<center>{| class="wikitable" align="center" style="color: blue; background-color:#ffffcc;" cellpadding="10"|+!colspan="6"|Преобразования, чтобы сформироватьверхнюю треугольную матрицу|-align="center" !class="dark"| <tex>a</tex> !class="dark"| <tex>b</tex> !class="dark"| <tex>c</tex> !class="dark"| <tex>d</tex> !class="green" style="font-weight:normal" style="background: #ddffdd;"| |Операция|-align="center" !class="dark" style="font-weight:normal"| <tex>1</tex> !class="dark" style="font-weight:normal"| <tex>0</tex> !class="dark" style="font-weight:normal"| <tex>1</tex> !class="dark" style="font-weight:normal"| <tex>1</tex> !class="green" style="font-weight:normal" style="background: #ddffdd;"| <tex>1</tex>| <tex>A</tex>|-align="center" !class="dark" style="font-weight:normal"| <tex>1</tex> !class="dark" style="font-weight:normal"| <tex>1</tex> !class="dark" style="font-weight:normal"| <tex>0</tex> !class="dark" style="font-weight:normal"| <tex>1</tex> !class="green" style="font-weight:normal" style="background: #ddffdd;"| <tex>0</tex>| <tex>C</tex>|-align="center" !class="dark" style="font-weight:normal"| <tex>1</tex> !class="dark" style="font-weight:normal"| <tex>1</tex> !class="dark" style="font-weight:normal"| <tex>1</tex> !class="dark" style="font-weight:normal"| <tex>0</tex> !class="green" style="font-weight:normal" style="background: #ddffdd;"| <tex>1</tex>| <tex>D</tex>|-align="center" !class="dark" style="font-weight:normal"| <tex>0</tex> !class="dark" style="font-weight:normal"| <tex>1</tex> !class="dark" style="font-weight:normal"| <tex>1</tex> !class="dark" style="font-weight:normal"| <tex>1</tex> !class="green" style="font-weight:normal" style="background: #ddffdd;"| <tex>0</tex>| <tex>B</tex>|}</center>!Поменяем местами строки <tex>B,\ C,\ D</tex>,<br>чтобы упростить получение верхней треугольной матрицы.|-align="center"!<center>{| class="wikitable" align="center" style="color: blue; background-color:#ffffcc;" cellpadding="10"|+|-align="center" !class="dark" style="font-weight:normal"| <tex>1</tex> !class="dark" style="font-weight:normal"| <tex>0</tex> !class="dark" style="font-weight:normal"| <tex>1</tex> !class="dark" style="font-weight:normal"| <tex>1</tex> !class="green" style="font-weight:normal" style="background: #ddffdd;"| <tex>1</tex>| <tex>A</tex>|-align="center" !class="dark" style="font-weight:normal"| <tex>0</tex> !class="dark" style="font-weight:normal"| <tex>1</tex> !class="dark" style="font-weight:normal"| <tex>1</tex> !class="dark" style="font-weight:normal"| <tex>0</tex> !class="green" style="font-weight:normal" style="background: #ddffdd;"| <tex>1</tex>| <tex>E=C \oplus A</tex>|-align="center" !class="dark" style="font-weight:normal"| <tex>0</tex> !class="dark" style="font-weight:normal"| <tex>1</tex> !class="dark" style="font-weight:normal"| <tex>0</tex> !class="dark" style="font-weight:normal"| <tex>1</tex> !class="green" style="font-weight:normal" style="background: #ddffdd;"| <tex>0</tex>| <tex>F=D \cong oplus A</tex>|-align="center" !class="dark" style="font-weight:normal"| <tex>0</tex> !class="dark" style="font-weight:normal"| <tex>1</tex> !class="dark" style="font-weight:normal"| <tex>1</tex> !class="dark" style="font-weight:normal"| <tex>1</tex> !class="green" style="font-weight:normal" style="background: #ddffdd;"| <tex>0</tex>| <tex>B</tex>|}</center>!Т.к. операция <tex>\oplus</tex> даёт <tex>0</tex> при одинаковых аргументах,применим её для строк <tex>A,\ C=E</tex> и <tex>A,\ D=F</tex>,<br>чтобы получить <tex>0</tex> в <tex>1</tex>-м столбце.|-align="center"!<center>{| class="wikitable" align="center" style="color: blue; background-color:#ffffcc;" cellpadding="10"|+|-align="center" !class="dark" style="font-weight:normal"| <tex>1</tex> !class="dark" style="font-weight:normal"| <tex>0</tex> !class="dark" style="font-weight:normal"| <tex>1</tex> !class="dark" style="font-weight:normal"| <tex>1</tex> !class="green" style="font-weight:normal" style="background: #ddffdd;"| <tex>1</tex>| <tex>A</tex>|-align="center" !class="dark" style="font-weight:normal"| <tex>0</tex> !class="dark" style="font-weight:normal"| <tex>1</tex> !class="dark" style="font-weight:normal"| <tex>1</tex> !class="dark" style="font-weight:normal"| <tex>0</tex> !class="green" style="font-weight:normal" style="background: #ddffdd;"| <tex>1</tex>| <tex>E</tex>|-align="center" !class="dark" style="font-weight:normal"| <tex>0</tex> !class="dark" style="font-weight:normal"| <tex>0</tex> !class="dark" style="font-weight:normal"| <tex>1</tex> !class="dark" style="font-weight:normal"| <tex>1</tex> !class="green" style="font-weight:normal" style="background: #ddffdd;"| <tex>1</tex>| <tex>G=F \oplus E</tex>|-align="center" !class="dark" style="font-weight:normal"| <tex>0</tex> !class="dark" style="font-weight:normal"| <tex>0</tex> !class="dark" style="font-weight:normal"| <tex>0</tex> !class="dark" style="font-weight:normal"| <tex>1</tex> !class="green" style="font-weight:normal" style="background: #ddffdd;"| <tex>1</tex>| <tex>H=B \oplus E</tex>|}</center>!Теперь применим <tex>\oplus</tex> для строк <tex>E,\ F=G</tex> и <tex>B,\ E=H</tex>,<br>чтобы получить <tex>0</tex> в <tex>2</tex>-м и <tex>3</tex>-м столбцах.|-align="center"!<center>{| class="wikitable" align="center" style="color: blue; background-color:#ffffcc;" cellpadding="10"|+!colspan="6"|Преобразования, чтобы сформироватьдиагональную матрицу|-align="center" !class="dark"| <tex>a</tex> !class="dark"| <tex>b</tex> !class="dark"| <tex>c</tex> !class="dark"| <tex>d</tex> !class="green" style="font-weight:normal" style="background: #ddffdd;"| |Операция|-align="center" !class="dark" style="font-weight:normal"| <tex>1</tex> !class="dark" style="font-weight:normal"| <tex>0</tex> !class="dark" style="font-weight:normal"| <tex>1</tex> !class="dark" style="font-weight:normal"| <tex>0</tex> !class="green" style="font-weight:normal" style="background: #ddffdd;"| <tex>0</tex>| <tex>I=A \oplus H</tex>|-align="center" !class="dark" style="font-weight:normal"| <tex>0</tex> !class="dark" style="font-weight:normal"| <tex>1</tex> !class="dark" style="font-weight:normal"| <tex>1</tex> !class="dark" style="font-weight:normal"| <tex>0</tex> !class="green" style="font-weight:normal" style="background: #ddffdd;"| <tex>1</tex>| <tex>E</tex>|-align="center" !class="dark" style="font-weight:normal"| <tex>0</tex> !class="dark" style="font-weight:normal"| <tex>0</tex> !class="dark" style="font-weight:normal"| <tex>1</tex> !class="dark" style="font-weight:normal"| <tex>0</tex> !class="green" style="font-weight:normal" style="background: #ddffdd;"| <tex>0</tex>| <tex>J=G \oplus H</tex>|-align="center" !class="dark" style="font-weight:normal"| <tex>0</tex> !class="dark" style="font-weight:normal"| <tex>0</tex> !class="dark" style="font-weight:normal"| <tex>0</tex> !class="dark" style="font-weight:normal"| <tex>1</tex> !class="green" style="font-weight:normal" style="background: #ddffdd;"| <tex>1</tex>| <tex>H</tex>|}</center>!Чтобы получить основную диагональную матрицу,<br>сделаем <tex>\oplus</tex> <tex>A,\ H=I</tex> и <tex>G,\ H=J</tex>,<br>чтобы получить <tex>0</tex> в <tex>4</tex>-м столбце выше диагонали.|-align="center"!<center>{| class="wikitable" align="center" style="color: blue; background-color:#ffffcc;" cellpadding="10"|+|-align="center" !class="dark" style="font-weight:normal"| <tex>1</tex> !class="dark" style="font-weight:normal"| <tex>0</tex> !class="dark" style="font-weight:normal"| <tex>0</tex> !class="dark" style="font-weight:normal"| <tex>0</tex> !class="green" style="font-weight:normal" style="background: #ddffdd;"| <tex>0</tex>| <tex>K=I \oplus J</tex>|-align="center" !class="dark" style="font-weight:normal"| <tex>0</tex> !class="dark" style="font-weight:normal"| <tex>1</tex> !class="dark" style="font-weight:normal"| <tex>0</tex> !class="dark" style="font-weight:normal"| <tex>0</tex> !class="green" style="font-weight:normal" style="background: #ddffdd;"| <tex>1</tex>| <tex>L=E \oplus J</tex>|-align="center" !class="dark" style="font-weight:normal"| <tex>0</tex> !class="dark" style="font-weight:normal"| <tex>0</tex> !class="dark" style="font-weight:normal"| <tex>1</tex> !class="dark" style="font-weight:normal"| <tex>0</tex> !class="green" style="font-weight:normal" style="background: #ddffdd;"| <tex>0</tex>| <tex>J</tex>|-align="center" !class="dark" style="font-weight:normal"| <tex>0</tex> !class="dark" style="font-weight:normal"| <tex>0</tex> !class="dark" style="font-weight:normal"| <tex>0</tex> !class="dark" style="font-weight:normal"| <tex>1</tex> !class="green" style="font-weight:normal" style="background: #ddffdd;"| <tex>1 </tex>| <tex>H</tex>
|}
!Осталось сделать <tex>\oplus</tex> <tex>I,\ J=K</tex> и <tex>E,\ J=L</tex>,<br>
потому что они отличаются в <tex>1</tex>-м и <tex>2</tex>-м столбцах.
|-align="center"
</center>
|}
===Решение===
Если <font color='red'>красный пункт</font> присутствует:<i> Решений нет</i><br>
Иначе:<br>
<tex>a=0=\mathtt {false}</tex><br>
<tex>b=1=\mathtt {true}</tex><br>
<tex>c=0=\mathtt {false}</tex><br>
<tex>d=1=\mathtt {true}</tex><br>
==Вычислительная сложность==
[[Файл:Булева выполнимость.png|400px|thumb|down|Формула с <tex>2</tex>-мя дизъюнктами может быть неудовлетворена(красный),<btex>3</tex>-<tex>\mathrm {3-SAT}</tex></b>(зелёный),<b><tex>\mathrm {XOR}</tex>-<tex>3</tex>-<tex>\mathrm {SAT}</tex></b>(синий) ,ИЛИили/И и <btex>1</tex>-<tex>\mathrm {1-in}</tex>-<tex>3</tex>-<tex>\mathrm {SAT}</tex></b>, в зависимости от количества переменных со значением TRUE <tex> \mathtt {true}</tex> в <tex>1</tex>-м (горизонтальном) и втором (вертикальном) конъюнкте.]]Поскольку <b><tex>a \oplus b \mathrm {a}oplus c</tex></b> <b>принимает значение <tex>\mathrm mathtt {XORtrue}</tex></b> <b>, если и только если <tex>\mathrm {b}1</tex></b> <b>из <tex>\mathrm {XOR}3</tex></b> <b>переменных <tex>\mathrm {a,\ b,\ c\}</tex></b> принимает значение <b><tex>\mathrm mathtt {TRUEtrue}</tex>, каждое решение в </btex>,если и только если 1 из 3 переменных {a,b,c} принимает значение <b/tex>-<tex>\mathrm {TRUEin}</tex>-</btex> ,каждое решение в 3<b/tex>-<tex>\mathrm {1-in-3-SAT}</tex></b> задачи для данной КНФ-формулы является также решением <b><tex>\mathrm {XOR}</tex>-<tex>3</tex>-<tex>\mathrm {SAT}</tex></b> задачи, и ,в свою очередь,обратное также верно. <br>Как следствие, для каждой КНФ-формулы, можно решить <b><tex>\mathrm {XOR}</tex></b>-<b><tex>\mathrm {3}</tex></b>-<b><tex>\mathrm {SAT}</tex></b> -задачу и на основании результатов сделать вывод, что либо <btex>3</tex>-<tex>\mathrm {3-SAT-задача}</tex></b> задача решаема или, что <btex>1</tex>-<tex>\mathrm {1-in}</tex>-<tex>3</tex>-<tex>\mathrm {SAT-задача}</tex>-задача нерешаема.</bbr> нерешаема.При условии ,что <tex>\mathrm {P}</tex>- и <tex>\mathrm {NP}</tex>-классы не равны,ни <tex>2</tex>-,ни Хорн-,ни <b><tex>\mathrm {XOR-SAT}</tex>-<tex>\mathrm {SAT}</btex> не являются задачи [[Класс NP|<tex>\mathrm {NP}</tex>-класса]],в отличии от <tex>\mathrm {SAT}</tex>.
== См. также ==
*[https://en.wikipedia.org/wiki/Boolean_satisfiability_problem Википедия — Boolean satisfiability problem]
* ''Cook, Stephen A.'' (1971). Proceedings of the 3rd Annual ACM Symposium on Theory of Computing: 151–158, 1971.
[[Категория: Дискретная математика и алгоритмы]]
[[Категория: Булевы функции ]]
96
правок

Навигация