Изменения

Перейти к: навигация, поиск

XOR-SAT

11 474 байта добавлено, 19:42, 4 сентября 2022
м
rollbackEdits.php mass rollback
{{Задача
|definition = <b><tex>\mathrm {XORSAT}</tex></b> (англ. ''XOR-satisfiability'') выполнимость функции — задача распределения аргументов в булевой [[КНФ|КНФ]] функции, записанной в виде XOR-КНФ, таким образом, чтобы результат данной функции был равен <tex> 1 </tex>.
}}
== Описание ==
Одним из особых случаев <b><tex>\mathrm {SAT}</tex></b> является класс задач, где каждый дизъюнкт конъюнкт содержит операции <tex>\oplus</tex> (т. е. исключающее или), а не (обычные) <tex>\lor</tex> операторы.(Формально, обобщенная КНФ с тернарным булевым оператором <tex> R </tex> работает только если <tex> 1 </tex> или <tex> 3 </tex> переменные дают <b><tex>\mathrm mathtt {TRUEtrue}</tex></b> в своих аргументах. ДизъюнктКонъюнкты,имеющие более <tex> 3 </tex> переменных могут быть преобразованы в сочетании с формулой преобразования с сохранением выполнимости булевой функции(ссылка на книгу ниже), т. е. <b><tex>\mathrm {XOR}</tex></b>-<b><tex>\mathrm {SAT}</tex></b> может быть снижена до <b><tex>\mathrm {XOR}</tex></b>-<b><tex>\mathrm {3}</tex></b>-<b><tex>\mathrm {SAT}</tex></b>)<ref>''Alfred V. Aho; John E. Hopcroft; Jeffrey D. Ullman (1974). ''The Design and Analysis of Computer Algorithms. Addison-Wesley.; здесь: Thm.10.4, 1974.</ref>
Это задача [[Класс P|<tex>\mathrm {P}</tex>-класса]], так как <tex>\mathrm {XOR}</tex>-<tex>\mathrm {SAT}</tex> формулу можно рассматривать как систему линейных уравнений по модулю <tex>2</tex>, которая, в свою очередь, может быть решена за <tex>O(n^3)</tex> методом Гаусса <ref>[https://ru.wikipedia.org/wiki/%D0%9C%D0%B5%D1%82%D0%BE%D0%B4_%D0%93%D0%B0%D1%83%D1%81%D1%81%D0%B0 Метод Гаусса]</ref>.Такое представление возможно на основе связи между Булевой алгеброй и Булевым [[Определение кольца, подкольца, изоморфизмы колец|кольцом]] <ref>[https://en.wikipedia.org/wiki/Boolean_algebra_(structure)#Boolean_rings Связь между Булевой алгеброй и Булевым кольцом]</ref> и том факте, что арифметика по модулю <tex>2</tex> образует конечное поле <ref>[https://ru.wikipedia.org/wiki/%D0%9A%D0%BE%D0%BD%D0%B5%D1%87%D0%BD%D0%BE%D0%B5_%D0%BF%D0%BE%D0%BB%D0%B5 Конечное поле ]</ref>.
Это задача [[Класс P|Р-класса]],так как ==Пример решения XORSAT=====Пример===<font color='red'>Красные пункты<b/font>могут быть добавлены для возможности представления КНФ-функции в виде <tex>\mathrm {XOR}</tex></b>-<b><tex>\mathrm {SAT}</tex>.{| class="wikitable"!<tex>(a \oplus b \oplus c) \land (b \oplus \neg c \oplus d) \land (a \oplus b \oplus \neg d) \land (a \oplus \neg b \oplus \neg c)</btex> формулу можно рассматривать как систему линейных уравнений по модулю 2,которая ,в свою очередь, может быть решена за ! style="background: #ffdddd;" |<tex>O\land (n^3\neg a \oplus b \oplus c)</tex> |}{| class="wikitable"|+!colspan="2"|Решение XOR-SAT задачи методом Гаусса|-align="center"!<refcenter>[https{| class="wikitable" align="center" style="color: blue; background-color:#ffffcc;" cellpadding="10"|+!colspan="2"|Система уравнений|-align="center"!Переменные|! width="20%" | Значение|-align="center"! <tex> a </tex> <tex>\oplus</ru.wikipedia.orgtex> <tex> c </wikitex> <tex>\oplus</%D0%9C%D0%B5%D1%82%D0%BE%D0%B4_%D0%93%D0%B0%D1%83%D1%81%D1%81%D0%B0]tex> <tex> d </reftex>.Такое представление возможно на основе связи между Булевой алгеброй и Булевым кольцом |<reftex>[https:=1</tex>|-align="center"! <tex> b </en.wikipedia.orgtex> <tex>\oplus</wikitex> <tex>\neg c </Boolean_algebra_(structure)#Boolean_rings]tex> <tex>\refoplus</tex> <tex> d </tex> |<tex>=1</tex> и тот факт,что арифметика по модулю 2 образует конечное поле |-align="center"! <reftex>[https:a </tex> <tex>\oplus</ru.wikipedia.orgtex> <tex> b </wikitex> <tex>\oplus</%D0%9A%D0%BE%D0%BD%D0%B5%D1%87%D0%BD%D0%BE%D0%B5_%D0%BF%D0%BE%D0%BB%D0%B5]tex> <tex>\refneg d </tex>.|<tex>=1</tex>==Решение XOR|-SAT задачи методом Гауссаalign="center"! <tex> \neg a </tex> <tex>\oplus</tex> <tex> \neg b </tex> <tex>\oplus</tex> <tex>\neg c </tex> |<tex>=1</tex> {| -align="center" class! style="wikitable collapsible collapsedbackground: #ffdddd;" |<tex> \neg a </tex> <tex>\oplus</tex> <tex> b </tex> <tex>\oplus</tex> <tex> c </tex>! style="text-alignbackground:left#ffdddd; margin: 1em"|<tex> =1 </tex>|-}</center>! Solving an XOR-SAT example(«<tex>1</tex>» означает «<tex> \mathtt {true}</tex>», «<tex>0</tex>» означает «<tex> \mathtt {false}<BR/tex>by Gaussian elimination»)Каждый конъюнкт ведет к одному уравнению.|-align="center"!|<center>{| alignclass="leftwikitable" classalign="collapsible collapsedcenter" style="textcolor: blue; background-aligncolor:left#ffffcc;" cellpadding="10"|-+! Given formulacolspan="2"|Нормированная система уравнений|-align="center"!Переменные| (! width="20%" means XOR, the {{color|#ff8080|red clause}} is optional)Значение|-align="center"| (''! <tex> a''⊕''</tex> <tex>\oplus</tex> <tex> c''⊕''</tex> <tex>\oplus</tex> <tex> d'') ∧ (''</tex> |<tex>=1</tex>|-align="center"! <tex> b''⊕¬''</tex> <tex>\oplus</tex> <tex> c''⊕''</tex> <tex>\oplus</tex> <tex> d'') ∧ (''</tex> |<tex>=0</tex>|-align="center"! <tex> a''⊕''</tex> <tex>\oplus</tex> <tex> b''⊕¬''</tex> <tex>\oplus</tex> <tex> d'') ∧ (''</tex> |<tex>=0</tex>|-align="center"! <tex> a''⊕¬''</tex> <tex>\oplus</tex> <tex> b''⊕¬''</tex> <tex>\oplus</tex> <tex> c'') {{color</tex> |<tex>=1</tex>|-align="center"! style="background: #ff8080ffdddd;" |∧ (¬''<tex> a''⊕''</tex> <tex>\oplus</tex> <tex> b''⊕''</tex> <tex>\oplus</tex> <tex> c'')}}</tex>! style="background: #ffdddd;" |<tex> =0 </tex>
|}
</center>!Используя свойства Булевых [[Определение кольца, подкольца, изоморфизмы колец|колец]] (<tex>\neg x=1 \oplus x</tex>, <tex>x \oplus x=1</tex>),<br>избавимся от отрицаний в нашей системе|-align="center"!|<center>{| alignclass="leftwikitable" classalign="collapsible collapsedcenter" style="textcolor: blue; background-aligncolor:left#ffffcc;" cellpadding="10"|-+! colspan="96" | Equation systemМатрица соответствующих коэффициентов|-align="center" !class="dark"| colspan<tex>a</tex> !class="9dark" | (<tex>b</tex> !class="1dark" means TRUE, | <tex>c</tex> !class="0dark" means FALSE)| <tex>d</tex>| !class="green" style="font-| colspanweight:normal" style="9background: #ddffdd;" | Each clause leads to one equation.|Строка|-align="center"| !class="dark" style="font-weight:normal"|| ''a'' || ⊕ || || ''c'' || ⊕ || || ''d'' || = <tex>1</tex> !class="dark" style="font-weight:normal"|-<tex>0</tex>| !class="dark" style="font-weight:normal"|| ''b'' || ⊕ || ¬ || ''c'' || ⊕ || || ''d'' || = <tex>1</tex> !class="dark" style="font-weight:normal"|-<tex>1</tex>| !class="green" style="font-weight:normal" style="background: #ddffdd;"|<tex>1</tex>| ''a'' || ⊕ || || ''b'' || ⊕ || ¬ || ''d'' |<tex>A</tex>| -align= 1"center" !class="dark" style="font-weight:normal"|<tex>0</tex> !class="dark" style="font-weight:normal"| <tex>1</tex>| !class="dark" style="font-weight:normal"|| ''a'' || ⊕ || ¬ || ''b'' || ⊕ || ¬ || ''c'' || = <tex>1</tex> !class="dark" style="font-weight:normal"|-<tex>1</tex>| {{color|!class="green" style="font-weight:normal" style="background: #ff8080ddffdd;"|¬}} <tex>0</tex>|<tex>B</tex>| {{color-align="center" !class="dark" style="font-weight:normal"|#ff8080<tex>1</tex> !class="dark" style="font-weight:normal"|''a''}} <tex>1</tex> !class="dark" style="font-weight:normal"|<tex>0</tex> !class="dark" style="font-weight:normal"| {{color|<tex>1</tex> !class="green" style="font-weight:normal" style="background: #ff8080ddffdd;"|⊕}} <tex>0</tex>|<tex>C</tex>| -align="center" !class="dark" style="font-weight:normal"|<tex>1</tex> !class="dark" style="font-weight:normal"| {{color<tex>1</tex> !class="dark" style="font-weight:normal"|#ff8080|''b''}} || {{color<tex>1</tex> !class="dark" style="font-weight:normal"|<tex>0</tex> !class="green" style="font-weight:normal" style="background: #ff8080ddffdd;"|⊕}} || || {{color|#ff8080|''c''}} || {{color|#ff8080<tex>1</tex>| ≃ 1}}<tex>D</tex>
|}
</center>!Составим матрицу по следующему правилу:Если переменная присутствовала в данном конъюнкте<br>ставим в ячейку <tex>1</tex>, иначе <tex>0</tex>|-align="center"!|<center>{| alignclass="leftwikitable" classalign="collapsible collapsedcenter" style="textcolor: blue; background-aligncolor:left#ffffcc;" cellpadding="10"|-+! colspan="6" | Normalized equation systemПреобразования, чтобы сформироватьверхнюю треугольную матрицу|-align="center"| colspan !class="6dark" | using properties of [[Boolean rings]] (¬''x''<tex>a</tex> !class=1⊕''x'', ''x''⊕''x''=0)"dark"|-<tex>b</tex> !class="dark"| ''a'' || ⊕ || ''<tex>c'' || ⊕ |</tex> !class="dark"| ''<tex>d'' </tex> !class="green" style="font-weight:normal" style="background: #ddffdd;"|| = '''1'''Операция|-align="center" !class="dark" style="font-weight:normal"| ''b'' <tex>1</tex> !class="dark" style="font-weight:normal"|<tex>0</tex> !class="dark" style="font-weight:normal"| <tex>1</tex> !class="dark" style="font-weight:normal"|<tex>1</tex> !class="green" style="font-weight:normal" style="background: #ddffdd;"| ''c'' || ⊕ || ''d'' <tex>1</tex>|<tex>A</tex>| -align= '''0'''"center" !class="dark" style="font-weight:normal"|<tex>1</tex> !class="dark" style="font-weight:normal"| <tex>1</tex> !class="dark" style="font-weight:normal"| ''a'' || ⊕ || ''b'' || ⊕ || ''d'' || = '''<tex>0'''</tex>| !class="dark" style="font-| ''a'' || ⊕ || ''b'' || ⊕ || ''c'' |weight:normal"| = '''<tex>1'''</tex>| !class="green" style="font-| {{color|weight:normal" style="background: #ff8080ddffdd;"|''a''}} <tex>0</tex>|<tex>C</tex>| {{color-align="center" !class="dark" style="font-weight:normal"|#ff8080<tex>1</tex> !class="dark" style="font-weight:normal"|⊕}} <tex>1</tex> !class="dark" style="font-weight:normal"|<tex>1</tex> !class="dark" style="font-weight:normal"| {{color|#ff8080|''b''}} || {{color|#ff8080|⊕}} || {{color|#ff8080|''c''}} || {{color|#ff8080| ≃ '''<tex>0'''}}</tex>| !class="green" style="font-| colspanweight:normal" style="6background: #ddffdd;" | (If the {{color|#ff8080|red equation}} is present, {{color|#ff8080<tex>1</tex>|it}} contradicts<tex>D</tex>|-align="center" !class="dark" style="font-weight:normal"| colspan<tex>0</tex> !class="dark" style="6font-weight:normal" | the last black one, so the system is unsolvable.<tex>1</tex> !class="dark" style="font-weight:normal"|-<tex>1</tex>| colspan !class="dark" style="6font-weight:normal" | Therefore, Gauss' algorithm is<tex>1</tex>| !class="green" style="font-| colspanweight:normal" style="6background: #ddffdd;" | used only for the black equations.)<tex>0</tex>| <tex>B</tex>
|}
</center>!Поменяем местами строки <tex>B,\ C,\ D</tex>,<br>чтобы упростить получение верхней треугольной матрицы.|-align="center"|!<center>{| alignclass="leftwikitable" classalign="collapsible collapsedcenter" style="textcolor: blue; background-aligncolor:left#ffffcc;"cellpadding="10"|+|-align="center" ! colspanclass="dark" style="6font-weight:normal" | Associated coefficient matrix<tex>1</tex> !class="dark" style="font-weight:normal"|<tex>0</tex> !class="dark" style="font-weight:normal"| &nbsp;<tex>1</tex> !class="dark" style="font-weight:normal"|-<tex>1</tex> ! ''a'' !! ''b'' !! ''c'' !! ''d'' !! !! lineclass="green" style="font-weight:normal" style="background: #ddffdd;"|-<tex>1</tex>| &nbsp;<tex>A</tex>|-align="center" !class="dark" style="font-weight:normal"| 1 || <tex>0 </tex> !class="dark" style="font-weight:normal"|<tex>1</tex> !class="dark" style="font-weight:normal"| <tex>1 </tex> !class="dark" style="font-weight:normal"|| 1<tex>0</tex> ! class="green" style="font-weight:normal" style="background: #ddffdd;"| <tex>1</tex>| <tex>E=C \oplus A</tex>|-align="center" !class="dark" style="font-weight:normal"| <tex>0 </tex> !class="dark" style="font-weight:normal"|| 1 || <tex>1 </tex> !class="dark" style="font-weight:normal"|<tex>0</tex> !class="dark" style="font-weight:normal"| <tex>1</tex> ! class="green" style="font-weight:normal" style="background: #ddffdd;"| <tex>0</tex>| B<tex>F=D \oplus A</tex>|-align="center" !class="dark" style="font-weight:normal"| 1 || 1 || <tex>0 </tex> !class="dark" style="font-weight:normal"|| <tex>1</tex> ! 0class="dark" style="font-weight:normal"| C<tex>1</tex>| !class="dark" style="font-| 1 || 1 |weight:normal"| <tex>1 </tex> !class="green" style="font-weight:normal" style="background: #ddffdd;"|| <tex>0! 1</tex>| D<tex>B</tex>
|}
</center>!Т.к. операция <tex>\oplus</tex> даёт <tex>0</tex> при одинаковых аргументах,применим её для строк <tex>A,\ C=E</tex> и <tex>A,\ D=F</tex>,<br>чтобы получить <tex>0</tex> в <tex>1</tex>-м столбце.|-align="center"!|<center>{| alignclass="leftwikitable" classalign="collapsible collapsedcenter" style="textcolor: blue; background-aligncolor:left#ffffcc;"|-! colspancellpadding="610" |Transforming to echelon form|-| &nbsp;+|-align="center" ! ''a'' !! ''b'' !! ''c'' !! ''d'' !! !! operation|class="dark" style="font-weight:normal"| &nbsp;<tex>1</tex>| !class="dark" style="font-| 1 |weight:normal"| <tex>0 || 1 || 1</tex> ! 1| A|class="dark" style="font-| 1 || 1 || 0 |weight:normal"| <tex>1</tex> ! 0| C|class="dark" style="font-| 1 || 1 |weight:normal"| <tex>1 || 0</tex> ! class="green" style="font-weight:normal" style="background: #ddffdd;"| <tex>1</tex>| D<tex>A</tex>|-align="center" !class="dark" style="font-weight:normal"| <tex>0 || 1 || 1 || 1</tex> ! 0| B (swapped)|class="dark" style="font-weight:normal"| &nbsp;<tex>1</tex>| !class="dark" style="font-| 1 || 0 || 1 |weight:normal"| <tex>1</tex> ! 1| A|class="dark" style="font-| 0 || 1 || 1 |weight:normal"| <tex>0</tex> ! class="green" style="font-weight:normal" style="background: #ddffdd;"| <tex>1</tex>| <tex>E = C⊕A</tex>|-align="center" !class="dark" style="font-weight:normal"| <tex>0 || 1 || 0 || 1</tex> ! 0| F class="dark" style= D⊕A|"font-weight:normal"| <tex>0 || 1 || 1 || 1</tex> ! 0| B|class="dark" style="font-weight:normal"| &nbsp;<tex>1</tex>| !class="dark" style="font-| 1 || 0 || 1 |weight:normal"| <tex>1</tex> ! class="green" style="font-weight:normal" style="background: #ddffdd;"| <tex>1</tex>| A<tex>G=F \oplus E</tex>|-align="center" !class="dark" style="font-weight:normal"| <tex>0 </tex> !class="dark" style="font-weight:normal"|| 1 || 1 || <tex>0</tex> ! 1| E|class="dark" style="font-weight:normal"| <tex>0 || 0 || 1 || 1</tex> ! 1| G class="dark" style= F⊕E|"font-| 0 || 0 || 0 |weight:normal"| <tex>1</tex> ! class="green" style="font-weight:normal" style="background: #ddffdd;"| <tex>1</tex>| <tex>H = B⊕EB \oplus E</tex>
|}
</center>!Теперь применим <tex>\oplus</tex> для строк <tex>E,\ F=G</tex> и <tex>B,\ E=H</tex>,<br>чтобы получить <tex>0</tex> в <tex>2</tex>-м и <tex>3</tex>-м столбцах.|-align="center"!|<center>{| alignclass="leftwikitable" classalign="collapsible collapsedcenter" style="textcolor: blue; background-aligncolor:left#ffffcc;" cellpadding="10"|-+! colspan="6" | Transforming to diagonal formПреобразования, чтобы сформировать|-| &nbsp;диагональную матрицу|-align="center" ! ''class="dark"| <tex>a'' </tex> !! ''class="dark"| <tex>b'' </tex> !! ''class="dark"| <tex>c'' </tex> !! ''class="dark"| <tex>d'' </tex> !! !! operationclass="green" style="font-weight:normal" style="background: #ddffdd;"|-| &nbsp;Операция|-align="center" !class="dark" style="font-weight:normal"| <tex>1 </tex> !class="dark" style="font-weight:normal"|| <tex>0 </tex> !class="dark" style="font-weight:normal"|| <tex>1 </tex> !class="dark" style="font-weight:normal"|| <tex>0</tex> ! class="green" style="font-weight:normal" style="background: #ddffdd;"| <tex>0</tex>| <tex>I = A⊕HA \oplus H</tex>|-align="center" !class="dark" style="font-weight:normal"| <tex>0 </tex> !class="dark" style="font-weight:normal"|| <tex>1 </tex> !class="dark" style="font-weight:normal"|| <tex>1 </tex> !class="dark" style="font-weight:normal"|| <tex>0</tex> ! class="green" style="font-weight:normal" style="background: #ddffdd;"| <tex>1</tex>| <tex>E</tex>|-align="center" !class="dark" style="font-weight:normal"| <tex>0 </tex> !class="dark" style="font-weight:normal"|| <tex>0 </tex> !class="dark" style="font-weight:normal"|| <tex>1 </tex> !class="dark" style="font-weight:normal"|| <tex>0</tex> ! 0| J class="green" style= G⊕H|"font-| 0 || 0 |weight:normal" style="background: #ddffdd;"| <tex>0 || 1! 1</tex>| <tex>J=G \oplus H</tex>|-align="center"| &nbsp;| !class="dark" style="font-| 1 || 0 || 0 |weight:normal"| <tex>0</tex> ! 0| K class="dark" style= I⊕J|"font-| 0 || 1 || 0 |weight:normal"| <tex>0</tex> ! 1| L class="dark" style= E⊕J|"font-| 0 || 0 || 1 |weight:normal"| <tex>0</tex> ! 0| J|class="dark" style="font-| 0 || 0 || 0 |weight:normal"| <tex>1</tex> ! class="green" style="font-weight:normal" style="background: #ddffdd;"| <tex>1</tex>| <tex>H|-</tex>
|}
</center>!Чтобы получить основную диагональную матрицу,<br>сделаем <tex>\oplus</tex> <tex>A,\ H=I</tex> и <tex>G,\ H=J</tex>,<br>чтобы получить <tex>0</tex> в <tex>4</tex>-м столбце выше диагонали.|-align="center"!|<center>{| alignclass="leftwikitable" classalign="collapsible collapsedcenter" style="textcolor: blue; background-aligncolor:left#ffffcc;" cellpadding="10"|+|-align="center" ! Solutionclass="dark" style="font-weight:normal"| <tex>1</tex> !class="dark" style="font-weight:normal"|<tex>0</tex> !class="dark" style="font-weight:normal"| <tex>0</tex> !class="dark" style="font-weight:normal"| If the {{color|<tex>0</tex> !class="green" style="font-weight:normal" style="background: #ff8080ddffdd;"|red clause}} is present: <tex>0</tex>|| Unsolvable<tex>K=I \oplus J</tex>|-align="center" !class="dark" style="font-weight:normal"| Else<tex>0</tex> !class="dark" style="font-weight: normal"|<tex>1</tex> !class="dark" style="font-weight:normal"| ''a'' <tex>0</tex> !class="dark" style= "font-weight:normal"| <tex>0 </tex> !class="green" style="font-weight:normal" style= FALSE"background: #ddffdd;"|-<tex>1</tex>| || ''b'' = 1 <tex>L= TRUEE \oplus J</tex>|-align="center" !class="dark" style="font-weight:normal"| || ''c'' <tex>0</tex> !class= 0 "dark" style= FALSE"font-weight:normal"|-<tex>0</tex>| || ''d'' !class= 1 "dark" style= TRUE"font-weight:normal"|-<tex>1</tex>| colspan !class="2dark" style="font-weight:normal" | '''As a consequence:'''<tex>0</tex>| !class="green" style="font-| colspanweight:normal" style="2background: #ddffdd;" | ''R''(''a'',''c'',''d'') ∧ ''R''(''b'',¬''c'',''d'') ∧ ''R''(''a'',''b'',¬''d'') ∧ ''R''(''a'',¬''b'',¬''c'') {{color|#ff8080<tex>0</tex>|∧ ''R''(¬''a'',''b'',''c'')}}<tex>J</tex>|-align="center"| colspan !class="2dark" | is not 1style="font-in-3-satisfiable,weight:normal"|-<tex>0</tex>| colspan !class="dark" style="2font-weight:normal" | while (''a''∨''c''∨''d'') ∧ (''b''∨¬''c''∨''d'') ∧ (''a''∨''b''∨¬''d'') ∧ (''a''∨¬''b''∨¬''c'')<tex>0</tex> !class="dark" style="font-weight:normal"|-<tex>0</tex>| colspan !class="dark" style="2font-weight:normal" | <tex>1</tex> is 3-satisfiable with ''a''!class=''c''"green" style=FALSE and ''b''"font-weight:normal" style=''d''=TRUE."background: #ddffdd;"| <tex>1</tex>| <tex>H</tex>
|}
!Осталось сделать <tex>\oplus</tex> <tex>I,\ J=K</tex> и <tex>E,\ J=L</tex>,<br>
потому что они отличаются в <tex>1</tex>-м и <tex>2</tex>-м столбцах.
|-align="center"
</center>
|}
===Решение===
Если <font color='red'>красный пункт</font> присутствует:<i> Решений нет</i><br>
Иначе:<br>
<tex>a=0=\mathtt {false}</tex><br>
<tex>b=1=\mathtt {true}</tex><br>
<tex>c=0=\mathtt {false}</tex><br>
<tex>d=1=\mathtt {true}</tex><br>
==Вычислительная сложность==
[[Файл:Булева выполнимость.png|400px|thumb|down|Формула с <tex>2</tex>-мя дизъюнктами может быть неудовлетворена(красный),<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>, в зависимости от количества переменных со значением TRUE <tex> \mathtt {true}</tex> в <tex>1</tex>-м (горизонтальном) и втором (вертикальном) дизъюнктеконъюнкте.]]Поскольку <tex>a XOR \oplus b XOR \oplus c </tex> принимает значение TRUE<tex> \mathtt {true}</tex>,если и только если <tex>1 </tex> из <tex>3 </tex> переменных <tex>\{a,\ b,\ c\} </tex> принимает значение TRUE<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>Как следствие, для каждой КНФ-формулы, можно решить <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>При условии ,что <tex>\mathrm {P}</tex>- и <tex>\mathrm {NP}</tex>-классы не равны,ни <tex>2</tex>-,ни Хорн-,ни <tex>\mathrm {XOR}</tex>-<tex>\mathrm {SAT }</tex> не являются задачи [[Класс NP|<tex>\mathrm {NP}</tex>-класса]],в отличии от <tex>\mathrm {SAT}</tex>.           
== См. также ==
*[https://en.wikipedia.org/wiki/Boolean_satisfiability_problem Википедия — Boolean satisfiability problem]
* ''Cook, Stephen A. (1971). ''Proceedings of the 3rd Annual ACM Symposium on Theory of Computing: 151–158, 1971.
[[Категория: Дискретная математика и алгоритмы]]
[[Категория: Булевы функции ]]
1632
правки

Навигация