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

Материал из Викиконспекты
Перейти к: навигация, поиск
(Решение XOR-SAT задачи методом Гаусса)
(Вычислительная сложность)
Строка 42: Строка 42:
  
 
==Вычислительная сложность==
 
==Вычислительная сложность==
[[Файл:Булева выполнимость.png|400px|thumb|down|Формула с 2-мя дизъюнктами может быть неудовлетворена(красный),<b><tex>\mathrm {3-SAT}</tex></b>(зелёный),<b><tex>\mathrm {XOR-3-SAT}</tex></b>(синий) ,ИЛИ/И <b><tex>\mathrm {1-in-3-SAT}</tex></b>, в зависимости от количества переменных со значением TRUE в 1-м (горизонтальном) и втором (вертикальном) конъюнкте.]]
+
[[Файл:Булева выполнимость.png|400px|thumb|down|Формула с 2-мя дизъюнктами может быть неудовлетворена(красный),<tex>3</tex>-<tex>\mathrm {SAT}</tex>(зелёный),<tex>\mathrm {XOR}</tex>-<tex>3</tex>-<tex>\mathrm {SAT}</tex>(синий) ,или/и <tex>1</tex>-<tex>\mathrm {in}</tex>-<tex>3</tex>-<tex>\mathrm {SAT}</tex>, в зависимости от количества переменных со значением <tex> \mathtt {true}</tex> в 1-м (горизонтальном) и втором (вертикальном) конъюнкте.]]
Поскольку <tex>a\ XOR\ b\ XOR\ c</tex> принимает значение <tex>\mathrm {TRUE}</tex>,если и только если 1 из 3 переменных {a,b,c} принимает значение <b><tex>\mathrm {TRUE}</tex></b> ,каждое решение в  <b><tex>\mathrm {1-in-3-SAT}</tex></b> задачи для данной КНФ-формулы является также решением <b><tex>\mathrm {XOR-3-SAT}</tex></b> задачи, и ,в свою очередь,обратное также верно.<br>
+
Поскольку <tex>a\ XOR\ b\ XOR\ c</tex> принимает значение <tex> \mathtt {true}</tex>,если и только если 1 из 3 переменных {<tex>a</tex>,<tex>b</tex>,<tex>c</tex>} принимает значение <tex> \mathtt {true}</tex> ,каждое решение в  <tex>1</tex>-<tex>\mathrm {in}</tex>-<tex>3</tex>-<tex>\mathrm {SAT}</tex> задачи для данной КНФ-формулы является также решением <tex>\mathrm {XOR}</tex>-<tex>3</tex>-<tex>\mathrm {SAT}</tex> задачи, и ,в свою очередь,обратное также верно.<br>
Как следствие, для каждой КНФ-формулы, можно решить <b><tex>\mathrm {XOR}</tex></b>-<b><tex>\mathrm {3}</tex></b>-<b><tex>\mathrm {SAT}</tex></b> -задачу и на основании результатов сделать вывод, что либо <b><tex>\mathrm {3}</tex></b>-<b><tex>\mathrm {SAT}</tex></b> решаема или, что <b><tex>\mathrm {1-in-3-SAT-задача}</tex></b> нерешаема.<br>
+
Как следствие, для каждой КНФ-формулы, можно решить <tex>\mathrm {XOR}</tex>-<tex>3</tex>-<tex>\mathrm {SAT}</tex>-задачу и на основании результатов сделать вывод, что либо <tex>3</tex>-<tex>\mathrm {SAT}</tex> задача решаема или, что <tex>1</tex>-<tex>\mathrm {in}</tex>-<tex>3</tex>-<tex>\mathrm {SAT}</tex>-задача нерешаема.<br>
При условии ,что P- и NP-классы не равны,ни 2-,ни Хорн-,ни <b><tex>\mathrm {XOR-SAT}</tex></b> не являются задачи [[Класс NP|NP-класса]],в отличии от SAT.
+
При условии ,что P- и NP-классы не равны,ни 2-,ни Хорн-,ни <tex>\mathrm {XOR}</tex>-<tex>\mathrm {SAT}</tex> не являются задачи [[Класс NP|NP-класса]],в отличии от <tex>\mathrm {SAT}</tex>.
  
 
== См. также ==
 
== См. также ==

Версия 11:31, 5 января 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 задачи методом Гаусса

Система уравнений
("[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]

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

Формула с 2-мя дизъюнктами может быть неудовлетворена(красный),[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] в 1-м (горизонтальном) и втором (вертикальном) конъюнкте.

Поскольку [math]a\ XOR\ b\ XOR\ c[/math] принимает значение [math] \mathtt {true}[/math],если и только если 1 из 3 переменных {[math]a[/math],[math]b[/math],[math]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]-задача нерешаема.
При условии ,что P- и NP-классы не равны,ни 2-,ни Хорн-,ни [math]\mathrm {XOR}[/math]-[math]\mathrm {SAT}[/math] не являются задачи NP-класса,в отличии от [math]\mathrm {SAT}[/math].

См. также

Примечания

  1. Alfred V. Aho; John E. Hopcroft; Jeffrey D. Ullman.The Design and Analysis of Computer Algorithms. Addison-Wesley.; здесь: Thm.10.4, 1974.
  2. Метод Гаусса
  3. Связь между Булевой алгеброй и Булевым кольцом
  4. Конечное поле

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