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

Материал из Викиконспекты
Перейти к: навигация, поиск
(→‎Решение XOR-SAT задачи методом Гаусса)
(→‎Решение XOR-SAT задачи методом Гаусса)
Строка 252: Строка 252:
 
  !class="dark"| <tex>c</tex>
 
  !class="dark"| <tex>c</tex>
 
  !class="dark"| <tex>d</tex>
 
  !class="dark"| <tex>d</tex>
−
  !class="green"|  
+
  !class="green" style="font-weight:normal" style="background: #ddffdd;"|  
 
|Операция
 
|Операция
 
|-align="center"
 
|-align="center"
Строка 275: Строка 275:
 
  !class="green" style="font-weight:normal" style="background: #ddffdd;"| <tex>0</tex>
 
  !class="green" style="font-weight:normal" style="background: #ddffdd;"| <tex>0</tex>
 
| <tex>J=G \oplus H</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>
 +
|}
 +
{| 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"
 
|-align="center"
 
  !class="dark" style="font-weight:normal"| <tex>0</tex>
 
  !class="dark" style="font-weight:normal"| <tex>0</tex>
Строка 284: Строка 315:
 
|}
 
|}
 
</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>
  
 
==Вычислительная сложность==
 
==Вычислительная сложность==

Версия 14:01, 5 января 2017

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


Описание

Одним из особых случаев [math]\mathrm {SAT}[/math] является класс задач, где каждый конъюнкт содержит операции [math]\oplus[/math] (т. е. исключающее или), а не (обычные) [math]\lor[/math] операторы.(Формально, обобщенная КНФ с тернарным булевым оператором R работает только если [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 {XOR}[/math]-[math]\mathrm {SAT}[/math] формулу можно рассматривать как систему линейных уравнений по модулю [math]2[/math],которая ,в свою очередь, может быть решена за [math]O(n^3)[/math] методом Гаусса [2].Такое представление возможно на основе связи между Булевой алгеброй и Булевым кольцом [3] и том факте,что арифметика по модулю [math]2[/math] образует конечное поле [4].

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

Система уравнений
("[math]1[/math]" означает «[math] \mathtt {true}[/math]», "[math]0[/math]" означает «[math] \mathtt {false}[/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]\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] \cong 1 [/math]
Нормированная система уравнений
Используя свойства Булевых колец

([math]\neg x=1 \oplus x[/math], [math]x \oplus x=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] \cong 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]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]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]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]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]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]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]R[/math]([math]a[/math],[math]c[/math],[math]d[/math])[math]\land[/math] [math]R[/math]([math]b[/math],[math]\neg c[/math],[math]d[/math])[math]\land[/math][math]R[/math]([math]a[/math],[math]b[/math],[math]\neg d[/math])[math]\land[/math][math]R[/math]([math]a[/math],[math]\neg b[/math],[math]\neg c[/math])∧ R(¬a,b,c)

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

Формула с [math]2[/math]-мя дизъюнктами может быть неудовлетворена(красный),[math]3[/math]-[math]\mathrm {SAT}[/math](зелёный),[math]\mathrm {XOR}[/math]-[math]3[/math]-[math]\mathrm {SAT}[/math](синий) ,или/и [math]1[/math]-[math]\mathrm {in}[/math]-[math]3[/math]-[math]\mathrm {SAT}[/math], в зависимости от количества переменных со значением [math] \mathtt {true}[/math] в [math]1[/math]-м (горизонтальном) и втором (вертикальном) конъюнкте.

Поскольку [math]a\ XOR\ b\ XOR\ c[/math] принимает значение [math] \mathtt {true}[/math],если и только если [math]1[/math] из [math]3[/math] переменных {[math]a[/math],[math]b[/math],[math]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]-задача нерешаема.
При условии ,что P- и NP-классы не равны,ни [math]2[/math]-,ни Хорн-,ни [math]\mathrm {XOR}[/math]-[math]\mathrm {SAT}[/math] не являются задачи NP-класса,в отличии от [math]\mathrm {SAT}[/math].

См. также

Примечания

  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. ↑ Конечное поле

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

Источник — «http://neerc.ifmo.ru/wiki/index.php?title=XOR-SAT&oldid=58772»