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

Материал из Викиконспекты
Перейти к: навигация, поиск
м (→‎Вычислительная сложность)
(→‎Решение XOR-SAT задачи методом Гаусса)
Строка 11: Строка 11:
 
Это задача [[Класс P|Р-класса]],так как <b><tex>\mathrm {XOR}</tex></b>-<b><tex>\mathrm {SAT}</tex></b> формулу можно рассматривать как систему линейных уравнений по модулю 2,которая ,в свою очередь, может быть решена за <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 ,kf,kf</ref>.Такое представление возможно на основе связи между Булевой алгеброй и Булевым кольцом <ref>https://en.wikipedia.org/wiki/Boolean_algebra_(structure)#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</ref>.
 
Это задача [[Класс P|Р-класса]],так как <b><tex>\mathrm {XOR}</tex></b>-<b><tex>\mathrm {SAT}</tex></b> формулу можно рассматривать как систему линейных уравнений по модулю 2,которая ,в свою очередь, может быть решена за <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 ,kf,kf</ref>.Такое представление возможно на основе связи между Булевой алгеброй и Булевым кольцом <ref>https://en.wikipedia.org/wiki/Boolean_algebra_(structure)#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</ref>.
  
−
==Решение XOR-SAT задачи методом Гаусса==
+
{| class="wikitable" align="center" style="color: blue; background-color:#ffffcc;" cellpadding="10"
−
 
+
|+
−
{| align="center" class="wikitable collapsible collapsed" style="text-align:left; margin: 1em"
+
!colspan="5"|Система уравнений
−
|-
+
|-align="center"
−
! Solving an XOR-SAT example<BR>by Gaussian elimination
+
!("<tex>1</tex>" означает «истинно», "<tex>0</tex>" означает «ложно»)
−
|-
+
Каждый конъюнкт ведет к одному уравнению.
 
|
 
|
−
{| align="center" class="collapsible collapsed" style="text-align:left"
+
|-align="center"
−
|-
+
!Переменные
−
! Given formula
+
|! width="20%" | Значения
−
|-
+
|-align="center"
−
| ("⊕" means XOR, the <font color=red> red clause </font> is optional)
+
! <tex> a </tex> <tex>\oplus</tex> <tex> c </tex> <tex>\oplus</tex> <tex> d </tex>  
−
|-
+
|<tex>=1</tex>
−
| (''a''⊕''c''⊕''d'') ∧ (''b''⊕¬''c''⊕''d'') ∧ (''a''⊕''b''⊕¬''d'') ∧ (''a''⊕¬''b''⊕¬''c'') <font color=red> ∧ (¬''a''⊕''b''⊕''c'') </font>
+
|-align="center"
−
|}
+
! <tex> b </tex> <tex>\oplus</tex> <tex>\neg c </tex> <tex>\oplus</tex> <tex> d </tex>  
−
|-
+
|<tex>=1</tex>
−
|
+
|-align="center"
−
{| align="left" class="collapsible collapsed" style="text-align:left"
+
! <tex> a </tex> <tex>\oplus</tex> <tex> b </tex> <tex>\oplus</tex> <tex>\neg d </tex>  
−
|-
+
|<tex>=1</tex>
−
! colspan="9" | Equation system
+
|-align="center"
−
|-
+
! <tex> \neg a </tex> <tex>\oplus</tex> <tex> \neg b </tex> <tex>\oplus</tex> <tex>\neg c </tex>
−
| colspan="9" | ("1" means TRUE, "0" means FALSE)
+
|<tex>=1</tex>
−
|-
+
|-align="center"
−
| colspan="9" | Each clause leads to one equation.
+
! 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>
−
|  ''a''  ⊕    ''c'' ⊕    ''d'' = 1
 
−
|-
 
−
|  ''b''  ⊕  ¬  ''c'' ⊕    ''d'' = 1
 
−
|-
 
−
|  ''a''  ⊕    ''b'' ⊕  ¬ ''d'' = 1
 
−
|-
 
−
|  ''a''  ⊕  ¬  ''b'' ⊕  ¬ ''c'' = 1
 
−
|-
 
−
|  <font color=red> ¬ </font> <font color=red> ''a'' </font> <font color=red> ⊕ </font> <font color=red> ''b'' </font> <font color=red> ⊕ </font> <font color=red> ''c'' </font><font color=red> ≃ 1 </font>
 
−
|-
 
−
|
 
−
{| align="left" class="collapsible collapsed" style="text-align:left"
 
−
|-
 
−
! colspan="6" | Normalized equation system
 
−
|-
 
−
| colspan="6" | using properties of [[Boolean rings]] (¬''x''=1⊕''x'', ''x''⊕''x''=0)
 
−
|-
 
−
| ''a'' || ⊕ || ''c'' || ⊕ || ''d'' || = '''1'''
 
−
|-
 
−
| ''b'' || ⊕ || ''c'' || ⊕ || ''d'' || = '''0'''
 
−
|-
 
−
| ''a'' || ⊕ || ''b'' || ⊕ || ''d'' || = '''0'''
 
−
|-
 
−
| ''a'' || ⊕ || ''b'' || ⊕ || ''c'' || = '''1'''
 
−
|-
 
−
| <font color=red> ''a'' </font> || <font color=red> ⊕ </font> || || <font color=red> ''b'' </font> || <font color=red> ⊕ </font> || || <font color=red> ''c'' </font> || <font color=red> ≃ ''0'' </font>
 
−
|-
 
−
| colspan="6" | (If the <font color=red> red equation </font> is present, <font color=red> it </font> contradicts
 
−
|-
 
−
| colspan="6" | the last black one, so the system is unsolvable.
 
−
|-
 
−
| colspan="6" | Therefore, Gauss' algorithm is
 
−
|-
 
−
| colspan="6" | used only for the black equations.)
 
−
|}
 
−
|-
 
−
|
 
−
{| align="left" class="collapsible collapsed" style="text-align:left"
 
−
|-
 
−
! colspan="6" | Associated coefficient matrix
 
−
|-
 
−
| &nbsp;
 
−
|-
 
−
! ''a'' !! ''b'' !! ''c'' !! ''d'' !!  !! line
 
−
|-
 
−
| &nbsp;
 
−
|-
 
−
| 1 || 0 || 1 || 1
 
−
! 1
 
−
| A
 
−
|-
 
−
| 0 || 1 || 1 || 1
 
−
! 0
 
−
| B
 
−
|-
 
−
| 1 || 1 || 0 || 1
 
−
! 0
 
−
| C
 
−
|-
 
−
| 1 || 1 || 1 || 0
 
−
! 1
 
−
| D
 
−
|}
 
−
|-
 
−
|
 
−
{| align="left" class="collapsible collapsed" style="text-align:left"
 
−
|-
 
−
! colspan="6" |Transforming to echelon form
 
−
|-
 
−
| &nbsp;
 
−
|-
 
−
! ''a'' !! ''b'' !! ''c'' !! ''d'' !!  !! operation
 
−
|-
 
−
| &nbsp;
 
−
|-
 
−
| 1 || 0 || 1 || 1
 
−
! 1
 
−
| A
 
−
|-
 
−
| 1 || 1 || 0 || 1
 
−
! 0
 
−
| C
 
−
|-
 
−
| 1 || 1 || 1 || 0
 
−
! 1
 
−
| D
 
−
|-
 
−
| 0 || 1 || 1 || 1
 
−
! 0
 
−
| B (swapped)
 
−
|-
 
−
| &nbsp;
 
−
|-
 
−
| 1 || 0 || 1 || 1
 
−
! 1
 
−
| A
 
−
|-
 
−
| 0 || 1 || 1 || 0
 
−
! 1
 
−
| E = C⊕A
 
−
|-
 
−
| 0 || 1 || 0 || 1
 
−
! 0
 
−
| F = D⊕A
 
−
|-
 
−
| 0 || 1 || 1 || 1
 
−
! 0
 
−
| B
 
−
|-
 
−
| &nbsp;
 
−
|-
 
−
| 1 || 0 || 1 || 1
 
−
! 1
 
−
| A
 
−
|-
 
−
| 0 || 1 || 1 || 0
 
−
! 1
 
−
| E
 
−
|-
 
−
| 0 || 0 || 1 || 1
 
−
! 1
 
−
| G = F⊕E
 
−
|-
 
−
| 0 || 0 || 0 || 1
 
−
! 1
 
−
| H = B⊕E
 
−
|}
 
−
|-
 
−
|
 
−
{| align="left" class="collapsible collapsed" style="text-align:left"
 
−
|-
 
−
! colspan="6" | Transforming to diagonal form
 
−
|-
 
−
| &nbsp;
 
−
|-
 
−
! ''a'' !! ''b'' !! ''c'' !! ''d'' !!  !! operation
 
−
|-
 
−
| &nbsp;
 
−
|-
 
−
| 1 || 0 || 1 || 0
 
−
! 0
 
−
| I = A⊕H
 
−
|-
 
−
| 0 || 1 || 1 || 0
 
−
! 1
 
−
| E
 
−
|-
 
−
| 0 || 0 || 1 || 0
 
−
! 0
 
−
| J = G⊕H
 
−
|-
 
−
| 0 || 0 || 0 || 1
 
−
! 1
 
−
| H
 
−
|-
 
−
| &nbsp;
 
−
|-
 
−
| 1 || 0 || 0 || 0
 
−
! 0
 
−
| K = I⊕J
 
−
|-
 
−
| 0 || 1 || 0 || 0
 
−
! 1
 
−
| L = E⊕J
 
−
|-
 
−
| 0 || 0 || 1 || 0
 
−
! 0
 
−
| J
 
−
|-
 
−
| 0 || 0 || 0 || 1
 
−
! 1
 
−
| H
 
−
|-
 
−
|}
 
−
|-
 
−
|
 
−
{| align="left" class="collapsible collapsed" style="text-align:left"
 
−
|-
 
−
! Solution:
 
−
|-
 
−
| If the <font color=red> red clause </font> is present: || Unsolvable
 
−
|-
 
−
| Else: || ''a'' = 0 = FALSE
 
−
|-
 
−
| || ''b'' = 1 = TRUE
 
−
|-
 
−
| || ''c'' = 0 = FALSE
 
−
|-
 
−
| || ''d'' = 1 = TRUE
 
−
|-
 
−
| colspan="2" | '''As a consequence:'''
 
−
|-
 
−
| colspan="2" | ''R''(''a'',''c'',''d'') ∧ ''R''(''b'',¬''c'',''d'') ∧ ''R''(''a'',''b'',¬''d'') ∧ ''R''(''a'',¬''b'',¬''c'')<font color=red> ∧ ''R''(¬''a'',''b'',''c'') </font>
 
−
|-
 
−
| colspan="2" | is not 1-in-3-satisfiable,
 
−
|-
 
−
| colspan="2" | while (''a''∨''c''∨''d'') ∧ (''b''∨¬''c''∨''d'') ∧ (''a''∨''b''∨¬''d'') ∧ (''a''∨¬''b''∨¬''c'')
 
−
|-
 
−
| colspan="2" |  is 3-satisfiable with ''a''=''c''=FALSE and ''b''=''d''=TRUE.
 
−
|}
 
 
|}
 
|}
  

Версия 23:59, 4 января 2017

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


Описание

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


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

Система уравнений
("[math]1[/math]" означает «истинно», "[math]0[/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]

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

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

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

См. также

Примечания

  1. ↑ Alfred V. Aho; John E. Hopcroft; Jeffrey D. Ullman (1974). The Design and Analysis of Computer Algorithms. Addison-Wesley.; здесь: Thm.10.4|методом Гаусса
  2. ↑ 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 ,kf,kf
  3. ↑ https://en.wikipedia.org/wiki/Boolean_algebra_(structure)#Boolean_rings
  4. ↑ 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

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

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