Материал из Викиконспекты
| Задача: |
| [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 задачи методом Гаусса
Solving an XOR-SAT example
by Gaussian elimination
|
| Given formula
|
| ("⊕" means XOR, the red clause is optional)
|
| (a⊕c⊕d) ∧ (b⊕¬c⊕d) ∧ (a⊕b⊕¬d) ∧ (a⊕¬b⊕¬c) Шаблон:Color
|
|
|
|
|
|
| Associated coefficient matrix
|
|
|
| a |
b |
c |
d |
|
line
|
|
|
| 1 |
0 |
1 |
1
|
1
|
A
|
| 0 |
1 |
1 |
1
|
0
|
B
|
| 1 |
1 |
0 |
1
|
0
|
C
|
| 1 |
1 |
1 |
0
|
1
|
D
|
|
| Transforming to echelon form
|
|
|
| a |
b |
c |
d |
|
operation
|
|
|
| 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)
|
|
|
| 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
|
|
|
| 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
|
|
| Transforming to diagonal form
|
|
|
| a |
b |
c |
d |
|
operation
|
|
|
| 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
|
|
|
| 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
|
|
| Solution:
|
| If the Шаблон:Color is present: |
Unsolvable
|
| Else: |
a = 0 = FALSE
|
| |
b = 1 = TRUE
|
| |
c = 0 = FALSE
|
| |
d = 1 = TRUE
|
| As a consequence:
|
| R(a,c,d) ∧ R(b,¬c,d) ∧ R(a,b,¬d) ∧ R(a,¬b,¬c) Шаблон:Color
|
| is not 1-in-3-satisfiable,
|
| while (a∨c∨d) ∧ (b∨¬c∨d) ∧ (a∨b∨¬d) ∧ (a∨¬b∨¬c)
|
| is 3-satisfiable with a=c=FALSE and b=d=TRUE.
|
|
Вычислительная сложность
Формула с 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.
См. такжеПримечанияИсточники информации
