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

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

Задача:

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

Содержание

1 Описание
2 Пример решения XORSAT
- 2.1 Пример
- 2.2 Решение
3 Вычислительная сложность
4 См. также
5 Примечания
6 Источники информации

Описание

Одним из особых случаев [math]\mathrm {SAT}[/math] является класс задач, где каждый конъюнкт содержит операции [math]\oplus[/math] (т. е. исключающее или), а не (обычные) [math]\lor[/math] операторы.Формально, обобщенная КНФ с тернарным булевым оператором [math] R[/math] работает только если [math] 1[/math] или [math] 3[/math] переменные дают [math] \mathtt {true}[/math] в своих аргументах. Конъюнкты, имеющие более [math] 3[/math] переменных могут быть преобразованы в сочетании с формулой преобразования с сохранением выполнимости булевой функции, т. е. [math]\mathrm {XOR}[/math]-[math]\mathrm {SAT}[/math] может быть снижена до [math]\mathrm {XOR}[/math]-[math]3[/math]-[math]\mathrm {SAT}[/math]^[1]

Это задача [math]\mathrm {P}[/math]-класса, так как [math]\mathrm {XOR}[/math]-[math]\mathrm {SAT}[/math] формулу можно рассматривать как систему линейных уравнений по модулю [math]2[/math], которая, в свою очередь, может быть решена за [math]O(n^3)[/math] методом Гаусса ^[2].Такое представление возможно на основе связи между Булевой алгеброй и Булевым кольцом ^[3] и том факте, что арифметика по модулю [math]2[/math] образует конечное поле ^[4].

Пример решения XORSAT

Пример

Красные пункты могут быть добавлены для возможности представления КНФ-функции в виде [math]\mathrm {XOR}[/math]-[math]\mathrm {SAT}[/math].

Решение XOR-SAT задачи методом Гаусса


Система уравнений
Переменные	Значение
[math] a [/math] [math]\oplus[/math] [math] c [/math] [math]\oplus[/math] [math] d [/math]	[math]=1[/math]
[math] b [/math] [math]\oplus[/math] [math]\neg c [/math] [math]\oplus[/math] [math] d [/math]	[math]=1[/math]
[math] a [/math] [math]\oplus[/math] [math] b [/math] [math]\oplus[/math] [math]\neg d [/math]	[math]=1[/math]
[math] \neg a [/math] [math]\oplus[/math] [math] \neg b [/math] [math]\oplus[/math] [math]\neg c [/math]	[math]=1[/math]
[math] \neg a [/math] [math]\oplus[/math] [math] b [/math] [math]\oplus[/math] [math] c [/math]	[math] =1 [/math]

(«» означает «», «» означает «»)

Каждый конъюнкт ведет к одному уравнению.


Нормированная система уравнений
Переменные	Значение
[math] a [/math] [math]\oplus[/math] [math] c [/math] [math]\oplus[/math] [math] d [/math]	[math]=1[/math]
[math] b [/math] [math]\oplus[/math] [math] c [/math] [math]\oplus[/math] [math] d [/math]	[math]=0[/math]
[math] a [/math] [math]\oplus[/math] [math] b [/math] [math]\oplus[/math] [math] d [/math]	[math]=0[/math]
[math] a [/math] [math]\oplus[/math] [math] b [/math] [math]\oplus[/math] [math] c [/math]	[math]=1[/math]
[math] a [/math] [math]\oplus[/math] [math] b [/math] [math]\oplus[/math] [math] c [/math]	[math] =0 [/math]

Используя свойства Булевых колец

([math]\neg x=1 \oplus x[/math], [math]x \oplus x=1[/math]),
избавимся от отрицаний в нашей системе


Матрица соответствующих коэффициентов
[math]a[/math]	[math]b[/math]	[math]c[/math]	[math]d[/math]		Строка
[math]1[/math]	[math]0[/math]	[math]1[/math]	[math]1[/math]	[math]1[/math]	[math]A[/math]
[math]0[/math]	[math]1[/math]	[math]1[/math]	[math]1[/math]	[math]0[/math]	[math]B[/math]
[math]1[/math]	[math]1[/math]	[math]0[/math]	[math]1[/math]	[math]0[/math]	[math]C[/math]
[math]1[/math]	[math]1[/math]	[math]1[/math]	[math]0[/math]	[math]1[/math]	[math]D[/math]

Составим матрицу по следующему правилу:

Если переменная присутствовала в данном конъюнкте
ставим в ячейку [math]1[/math], иначе [math]0[/math]


Преобразования, чтобы сформировать верхнюю треугольную матрицу
[math]a[/math]	[math]b[/math]	[math]c[/math]	[math]d[/math]		Операция
[math]1[/math]	[math]0[/math]	[math]1[/math]	[math]1[/math]	[math]1[/math]	[math]A[/math]
[math]1[/math]	[math]1[/math]	[math]0[/math]	[math]1[/math]	[math]0[/math]	[math]C[/math]
[math]1[/math]	[math]1[/math]	[math]1[/math]	[math]0[/math]	[math]1[/math]	[math]D[/math]
[math]0[/math]	[math]1[/math]	[math]1[/math]	[math]1[/math]	[math]0[/math]	[math]B[/math]

Поменяем местами строки ,

чтобы упростить получение верхней треугольной матрицы.


[math]1[/math]	[math]0[/math]	[math]1[/math]	[math]1[/math]	[math]1[/math]	[math]A[/math]
[math]0[/math]	[math]1[/math]	[math]1[/math]	[math]0[/math]	[math]1[/math]	[math]E=C \oplus A[/math]
[math]0[/math]	[math]1[/math]	[math]0[/math]	[math]1[/math]	[math]0[/math]	[math]F=D \oplus A[/math]
[math]0[/math]	[math]1[/math]	[math]1[/math]	[math]1[/math]	[math]0[/math]	[math]B[/math]

Т.к. операция даёт при одинаковых аргументах,

применим её для строк [math]A,\ C=E[/math] и [math]A,\ D=F[/math],
чтобы получить [math]0[/math] в [math]1[/math]-м столбце.


[math]1[/math]	[math]0[/math]	[math]1[/math]	[math]1[/math]	[math]1[/math]	[math]A[/math]
[math]0[/math]	[math]1[/math]	[math]1[/math]	[math]0[/math]	[math]1[/math]	[math]E[/math]
[math]0[/math]	[math]0[/math]	[math]1[/math]	[math]1[/math]	[math]1[/math]	[math]G=F \oplus E[/math]
[math]0[/math]	[math]0[/math]	[math]0[/math]	[math]1[/math]	[math]1[/math]	[math]H=B \oplus E[/math]

Теперь применим для строк и ,

чтобы получить [math]0[/math] в [math]2[/math]-м и [math]3[/math]-м столбцах.


Преобразования, чтобы сформировать диагональную матрицу
[math]a[/math]	[math]b[/math]	[math]c[/math]	[math]d[/math]		Операция
[math]1[/math]	[math]0[/math]	[math]1[/math]	[math]0[/math]	[math]0[/math]	[math]I=A \oplus H[/math]
[math]0[/math]	[math]1[/math]	[math]1[/math]	[math]0[/math]	[math]1[/math]	[math]E[/math]
[math]0[/math]	[math]0[/math]	[math]1[/math]	[math]0[/math]	[math]0[/math]	[math]J=G \oplus H[/math]
[math]0[/math]	[math]0[/math]	[math]0[/math]	[math]1[/math]	[math]1[/math]	[math]H[/math]

Чтобы получить основную диагональную матрицу,

сделаем [math]\oplus[/math] [math]A,\ H=I[/math] и [math]G,\ H=J[/math],
чтобы получить [math]0[/math] в [math]4[/math]-м столбце выше диагонали.


[math]1[/math]	[math]0[/math]	[math]0[/math]	[math]0[/math]	[math]0[/math]	[math]K=I \oplus J[/math]
[math]0[/math]	[math]1[/math]	[math]0[/math]	[math]0[/math]	[math]1[/math]	[math]L=E \oplus J[/math]
[math]0[/math]	[math]0[/math]	[math]1[/math]	[math]0[/math]	[math]0[/math]	[math]J[/math]
[math]0[/math]	[math]0[/math]	[math]0[/math]	[math]1[/math]	[math]1[/math]	[math]H[/math]

Осталось сделать и ,

потому что они отличаются в [math]1[/math]-м и [math]2[/math]-м столбцах.

Решение

Если красный пункт присутствует: Решений нет
Иначе:
[math]a=0=\mathtt {false}[/math]
[math]b=1=\mathtt {true}[/math]
[math]c=0=\mathtt {false}[/math]
[math]d=1=\mathtt {true}[/math]

Вычислительная сложность

Формула с -мя дизъюнктами может быть неудовлетворена(красный), -(зелёный), --(синий), или/и ---, в зависимости от количества переменных со значением в -м (горизонтальном) и втором (вертикальном) конъюнкте.

Поскольку [math]a \oplus b \oplus c[/math] принимает значение [math] \mathtt {true}[/math], если и только если [math]1[/math] из [math]3[/math] переменных [math]\{a,\ b,\ c\}[/math] принимает значение [math] \mathtt {true}[/math], каждое решение в [math]1[/math]-[math]\mathrm {in}[/math]-[math]3[/math]-[math]\mathrm {SAT}[/math] задачи для данной КНФ-формулы является также решением [math]\mathrm {XOR}[/math]-[math]3[/math]-[math]\mathrm {SAT}[/math] задачи, и, в свою очередь, обратное также верно.
Как следствие, для каждой КНФ-формулы, можно решить [math]\mathrm {XOR}[/math]-[math]3[/math]-[math]\mathrm {SAT}[/math]-задачу и на основании результатов сделать вывод, что либо [math]3[/math]-[math]\mathrm {SAT}[/math] задача решаема или, что [math]1[/math]-[math]\mathrm {in}[/math]-[math]3[/math]-[math]\mathrm {SAT}[/math]-задача нерешаема.
При условии, что [math]\mathrm {P}[/math]- и [math]\mathrm {NP}[/math]-классы не равны, ни [math]2[/math]-, ни Хорн-, ни [math]\mathrm {XOR}[/math]-[math]\mathrm {SAT}[/math] не являются задачи [math]\mathrm {NP}[/math]-класса, в отличии от [math]\mathrm {SAT}[/math].

См. также

Примечания

↑ Alfred V. Aho; John E. Hopcroft; Jeffrey D. Ullman.The Design and Analysis of Computer Algorithms. Addison-Wesley.; здесь: Thm.10.4, 1974.
↑ Метод Гаусса
↑ Связь между Булевой алгеброй и Булевым кольцом
↑ Конечное поле

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

Википедия — Boolean satisfiability problem
Cook, Stephen A.Proceedings of the 3rd Annual ACM Symposium on Theory of Computing: 151–158, 1971.

[1] Alfred V. Aho; John E. Hopcroft; Jeffrey D. Ullman.The Design and Analysis of Computer Algorithms. Addison-Wesley.; здесь: Thm.10.4, 1974.

[2] Метод Гаусса

[3] Связь между Булевой алгеброй и Булевым кольцом

[4] Конечное поле

[1]

[2]

[3]

[4]

@@ Строка 1: / Строка 1: @@
 {{Задача
-|definition = <b><tex>\mathrm {XORSAT}</tex></b> (XOR-satisfiability) выполнимость функции — задача распределения аргументов в булевой [[КНФ|КНФ]] функции, записанной в виде XOR-КНФ, таким образом, чтобы результат данной функции был равен <tex> 1 </tex>.
+|definition = <b><tex>\mathrm {XORSAT}</tex></b> (англ. ''XOR-satisfiability'') выполнимость функции — задача распределения аргументов в булевой [[КНФ|КНФ]] функции, записанной в виде XOR-КНФ, таким образом, чтобы результат данной функции был равен <tex> 1 </tex>.
 }}
@@ Строка 6: / Строка 6: @@
 == Описание ==
-Одним из особых случаев <tex>\mathrm {SAT}</tex> является класс задач, где каждый конъюнкт содержит операции <tex>\oplus</tex> (т. е. исключающее или), а не (обычные) <tex>\lor</tex> операторы.(Формально, обобщенная КНФ с тернарным  булевым  оператором <tex> \mathrm {R}</tex> работает  только если <tex> 1</tex> или <tex> 3</tex> переменные дают <tex> \mathtt {true}</tex> в своих аргументах. Конъюнкты,имеющие более <tex> 3</tex> переменных могут быть преобразованы в сочетании с формулой преобразования с сохранением выполнимости булевой функции, т. е. <tex>\mathrm {XOR}</tex>-<tex>\mathrm {SAT}</tex>  может быть снижена до <tex>\mathrm {XOR}</tex>-<tex>3</tex>-<tex>\mathrm {SAT}</tex>)<ref>''Alfred V. Aho; John E. Hopcroft; Jeffrey D. Ullman.''The Design and Analysis of Computer Algorithms. Addison-Wesley.; здесь: Thm.10.4, 1974.</ref>
+Одним из особых случаев <tex>\mathrm {SAT}</tex> является класс задач, где каждый конъюнкт содержит операции <tex>\oplus</tex> (т. е. исключающее или), а не (обычные) <tex>\lor</tex> операторы.Формально, обобщенная КНФ с тернарным  булевым  оператором <tex> R</tex> работает  только если <tex> 1</tex> или <tex> 3</tex> переменные дают <tex> \mathtt {true}</tex> в своих аргументах. Конъюнкты, имеющие более <tex> 3</tex> переменных могут быть преобразованы в сочетании с формулой преобразования с сохранением выполнимости булевой функции, т. е. <tex>\mathrm {XOR}</tex>-<tex>\mathrm {SAT}</tex>  может быть снижена до <tex>\mathrm {XOR}</tex>-<tex>3</tex>-<tex>\mathrm {SAT}</tex><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|Р-класса]], так как <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>.
+==Пример решения XORSAT==
+===Пример===
-==Решение XOR-SAT задачи методом Гаусса==
+<font color='red'>Красные пункты</font> могут быть добавлены для возможности представления КНФ-функции в виде <tex>\mathrm {XOR}</tex>-<tex>\mathrm {SAT}</tex>.
+{| class="wikitable"
+!<tex>(a \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;" |<tex> \land (\neg a \oplus  b \oplus c) </tex>
+|}
+{| class="wikitable"
+|+
+!colspan="2"|Решение XOR-SAT задачи методом Гаусса
+|-align="center"
+!
 <center>
 {| class="wikitable" align="center" style="color: blue; background-color:#ffffcc;" cellpadding="10"
 |+
 !colspan="2"|Система уравнений
-|-align="center"
-!("<tex>1</tex>" означает «<tex> \mathtt {true}</tex>», "<tex>0</tex>" означает «<tex> \mathtt {false}</tex>»)
-Каждый конъюнкт ведет к одному уравнению.
-|
 |-align="center"
 !Переменные
@@ Строка 37: / Строка 43: @@
 |-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> \cong 1 </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"
-!Используя свойства Булевых колец
-(<tex>\neg x=1 \oplus x</tex>, <tex>x \oplus x=1</tex>)
-|
 |-align="center"
 !Переменные
@@ Строка 64: / Строка 71: @@
 |-align="center"
 ! style="background: #ffdddd;" |<tex> a </tex> <tex>\oplus</tex> <tex>  b </tex>  <tex>\oplus</tex>  <tex> c </tex>
-! style="background: #ffdddd;" |<tex> \cong 0 </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"
 |+
@@ Строка 75: / Строка 88: @@
   !class="dark"| <tex>c</tex>
   !class="dark"| <tex>d</tex>
   !class="green" style="font-weight:normal" style="background: #ddffdd;"|
 |Строка
 |-align="center"
@@ Строка 106: / Строка 119: @@
 | <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"
 |+
@@ Строка 147: / Строка 166: @@
 | <tex>B</tex>
 |}
+</center>
-{| class="wikitable" align="center" style="color: blue; background-color:#ffffcc;" cellpadding="10"
+!Поменяем местами строки <tex>B,\ C,\ D</tex>,<br>
-|+
+чтобы упростить получение верхней треугольной матрицы.
 |-align="center"
- !class="dark" style="font-weight:normal"| <tex>1</tex>
+!
- !class="dark" style="font-weight:normal"| <tex>0</tex>
+<center>
- !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>
-|}
 {| class="wikitable" align="center" style="color: blue; background-color:#ffffcc;" cellpadding="10"
 |+
@@ Строка 211: / Строка 203: @@
 | <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"
 |+
@@ Строка 243: / Строка 241: @@
 | <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"
 |+
@@ Строка 283: / Строка 287: @@
 | <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"
 |+
@@ Строка 314: / Строка 325: @@
 | <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>
+|}
-Следствие:<tex>R</tex>(<tex>a</tex>,<tex>c</tex>,<tex>d</tex>)<tex>\land</tex> <tex>R</tex>(<tex>b</tex>,<tex>\neg c</tex>,<tex>d</tex>)<tex>\land</tex><tex>R</tex>(<tex>a</tex>,<tex>b</tex>,<tex>\neg d</tex>)<tex>\land</tex><tex>R</tex>(<tex>a</tex>,<tex>\neg b</tex>,<tex>\neg c</tex>)<font color='red'>∧ R(¬a,b,c)</font>
+===Решение===
+Если <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>-мя дизъюнктами может быть неудовлетворена(красный),<tex>3</tex>-<tex>\mathrm {SAT}</tex>(зелёный),<tex>\mathrm {XOR}</tex>-<tex>3</tex>-<tex>\mathrm {SAT}</tex>(синий) ,или/и <tex>1</tex>-<tex>\mathrm {in}</tex>-<tex>3</tex>-<tex>\mathrm {SAT}</tex>, в зависимости от количества переменных со значением <tex> \mathtt {true}</tex> в <tex>1</tex>-м (горизонтальном) и втором (вертикальном) конъюнкте.]]
+[[Файл:Булева выполнимость.png|400px|thumb|down|Формула с <tex>2</tex>-мя дизъюнктами может быть неудовлетворена(красный), <tex>3</tex>-<tex>\mathrm {SAT}</tex>(зелёный), <tex>\mathrm {XOR}</tex>-<tex>3</tex>-<tex>\mathrm {SAT}</tex>(синий), или/и <tex>1</tex>-<tex>\mathrm {in}</tex>-<tex>3</tex>-<tex>\mathrm {SAT}</tex>, в зависимости от количества переменных со значением <tex> \mathtt {true}</tex> в <tex>1</tex>-м (горизонтальном) и втором (вертикальном) конъюнкте.]]
-Поскольку <tex>a\ XOR\ b\ XOR\ c</tex> принимает значение <tex> \mathtt {true}</tex>,если и только если <tex>1</tex> из <tex>3</tex> переменных {<tex>a</tex>,<tex>b</tex>,<tex>c</tex>} принимает значение <tex> \mathtt {true}</tex> ,каждое решение в  <tex>1</tex>-<tex>\mathrm {in}</tex>-<tex>3</tex>-<tex>\mathrm {SAT}</tex> задачи для данной КНФ-формулы является также решением <tex>\mathrm {XOR}</tex>-<tex>3</tex>-<tex>\mathrm {SAT}</tex> задачи, и ,в свою очередь,обратное также верно.<br>
+Поскольку <tex>a \oplus b \oplus c</tex> принимает значение <tex> \mathtt {true}</tex>, если и только если <tex>1</tex> из <tex>3</tex> переменных <tex>\{a,\ b,\ c\}</tex> принимает значение <tex> \mathtt {true}</tex>, каждое решение в  <tex>1</tex>-<tex>\mathrm {in}</tex>-<tex>3</tex>-<tex>\mathrm {SAT}</tex> задачи для данной КНФ-формулы является также решением <tex>\mathrm {XOR}</tex>-<tex>3</tex>-<tex>\mathrm {SAT}</tex> задачи, и, в свою очередь, обратное также верно.<br>
 Как следствие, для каждой КНФ-формулы, можно решить <tex>\mathrm {XOR}</tex>-<tex>3</tex>-<tex>\mathrm {SAT}</tex>-задачу и на основании результатов сделать вывод, что либо <tex>3</tex>-<tex>\mathrm {SAT}</tex> задача решаема или, что <tex>1</tex>-<tex>\mathrm {in}</tex>-<tex>3</tex>-<tex>\mathrm {SAT}</tex>-задача нерешаема.<br>
-При условии ,что P- и NP-классы не равны,ни <tex>2</tex>-,ни Хорн-,ни <tex>\mathrm {XOR}</tex>-<tex>\mathrm {SAT}</tex> не являются задачи [[Класс NP|NP-класса]],в отличии от <tex>\mathrm {SAT}</tex>.
+При условии, что <tex>\mathrm {P}</tex>- и <tex>\mathrm {NP}</tex>-классы не равны, ни <tex>2</tex>-, ни Хорн-, ни <tex>\mathrm {XOR}</tex>-<tex>\mathrm {SAT}</tex> не являются задачи [[Класс NP|<tex>\mathrm {NP}</tex>-класса]], в отличии от <tex>\mathrm {SAT}</tex>.
 == См. также ==
@@ Строка 340: / Строка 360: @@
 [[Категория: Дискретная математика и алгоритмы]]
-[[Категория: Булевы функции ]]
+[[Категория: Булевы функции]]

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

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

Содержание

Описание

Пример решения XORSAT

Пример

Решение

Вычислительная сложность

См. также

Примечания

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

Навигация

Персональные инструменты

Пространства имён

Варианты

Просмотры

Ещё

Поиск

Навигация

Инструменты