XOR-SAT

Задача:

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

Описание

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

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

Решение 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 \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] не являются задачи NP-класса, в отличии от [math]\mathrm {SAT}[/math].

См. также

• Специальные формы КНФ
• 2SAT
• NP-полнота задачи о выполнимости булевой формулы в форме 3-КНФ

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

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