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

Материал из Викиконспекты
Перейти к: навигация, поиск
м (Описание)
(Решение XOR-SAT задачи методом Гаусса)
Строка 24: Строка 24:
 
| ("⊕" means XOR, the <font color=red> red clause </font> is optional)
 
| ("⊕" means XOR, the <font color=red> red clause </font> is optional)
 
|-
 
|-
| (''a''⊕''c''⊕''d'') ∧ (''b''⊕¬''c''⊕''d'') ∧ (''a''⊕''b''⊕¬''d'') ∧ (''a''⊕¬''b''⊕¬''c'') {{color|#ff8080|∧ (¬''a''⊕''b''⊕''c'')}}
+
| (''a''⊕''c''⊕''d'') ∧ (''b''⊕¬''c''⊕''d'') ∧ (''a''⊕''b''⊕¬''d'') ∧ (''a''⊕¬''b''⊕¬''c'') <font color=red> ∧ (¬''a''⊕''b''⊕''c'') </font>
 
|}
 
|}
 
|-
 
|-
Строка 36: Строка 36:
 
| colspan="9" | Each clause leads to one equation.
 
| colspan="9" | Each clause leads to one equation.
 
|-
 
|-
| || ''a'' || ||  || ''c'' || ||  || ''d'' || = 1
+
|   ''a''     ''c'' ⊕   ''d'' = 1
 
|-
 
|-
| || ''b'' || || ¬ || ''c'' || ||  || ''d'' || = 1
+
|   ''b'' ¬ ''c'' ⊕   ''d'' = 1
 
|-
 
|-
| || ''a'' || ||  || ''b'' || || ¬ || ''d'' || = 1
+
|   ''a''     ''b'' ⊕ ¬ ''d'' = 1
 
|-
 
|-
| || ''a'' || || ¬ || ''b'' || || ¬ || ''c'' || = 1
+
|   ''a'' ¬ ''b'' ⊕ ¬ ''c'' = 1
 
|-
 
|-
{{color|#ff8080|¬}} || {{color|#ff8080|''a''}} || {{color|#ff8080|}} || || {{color|#ff8080|''b''}} || {{color|#ff8080|}} || || {{color|#ff8080|''c''}} || {{color|#ff8080| ≃ 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>
|}
 
 
|-
 
|-
 
|
 
|
Строка 62: Строка 61:
 
| ''a'' || ⊕ || ''b'' || ⊕ || ''c'' || = '''1'''
 
| ''a'' || ⊕ || ''b'' || ⊕ || ''c'' || = '''1'''
 
|-
 
|-
| {{color|#ff8080|''a''}} || {{color|#ff8080|⊕}}  || {{color|#ff8080|''b''}} || {{color|#ff8080|⊕}} || {{color|#ff8080|''c''}} || {{color|#ff8080| '''0'''}}
+
| <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 {{color|#ff8080|red equation}} is present, {{color|#ff8080|it}} contradicts
+
| 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" | the last black one, so the system is unsolvable.
Строка 217: Строка 216:
 
! Solution:
 
! Solution:
 
|-
 
|-
| If the {{color|#ff8080|red clause}} is present: || Unsolvable
+
| If the <font color=red> red clause </font> is present: || Unsolvable
 
|-
 
|-
 
| Else: || ''a'' = 0 = FALSE
 
| Else: || ''a'' = 0 = FALSE
Строка 229: Строка 228:
 
| colspan="2" | '''As a consequence:'''
 
| colspan="2" | '''As a consequence:'''
 
|-
 
|-
| colspan="2" | ''R''(''a'',''c'',''d'') ∧ ''R''(''b'',¬''c'',''d'') ∧ ''R''(''a'',''b'',¬''d'') ∧ ''R''(''a'',¬''b'',¬''c'') {{color|#ff8080|∧ ''R''(¬''a'',''b'',''c'')}}
+
| 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" | is not 1-in-3-satisfiable,

Версия 21:07, 3 января 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].

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