XOR-SAT

Задача:

[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])

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

Решение 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) ∧ (¬a⊕b⊕c)
Equation system ("1" means TRUE, "0" means FALSE) Each clause leads to one equation. a ⊕ c ⊕ d = 1 b ⊕ ¬ c ⊕ d = 1 a ⊕ b ⊕ ¬ d = 1 a ⊕ ¬ b ⊕ ¬ c = 1 ¬ a ⊕ b ⊕ c ≃ 1 Normalized equation system 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 a ⊕ b ⊕ c ≃ 0 (If the red equation is present, it contradicts the last black one, so the system is unsolvable. Therefore, Gauss' algorithm is used only for the black equations.) 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 red clause 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) ∧ R(¬a,b,c) 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. См. также Специальные формы КНФ 2SAT NP-полнота задачи о выполнимости булевой формулы в форме 3-КНФ Примечания Источники информации Википедия — Boolean satisfiability problem Cook, Stephen A. (1971). Proceedings of the 3rd Annual ACM Symposium on Theory of Computing: 151–158.