62
правки
Изменения
Новая страница: «{{Задача |definition = <b><tex>\mathrm {XORSAT}</tex></b> (XOR-satisfiability) выполнимость функции — задача распределе...»
{{Задача
|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> операторы.(Формально, обобщенная КНФ с тернарным булевым оператором R работает только если 1 или 3 переменные дают TRUE в своих аргументах. Дизъюнкт,имеющие более 3 переменных могут быть преобразованы в сочетании с формулой преобразования с сохранением выполнимости булевой функции(ссылка на книгу ниже), т. е. XOR-SAT может быть снижена до XOR-3-SAT)<ref>Alfred V. Aho; John E. Hopcroft; Jeffrey D. Ullman (1974). The Design and Analysis of Computer Algorithms. Addison-Wesley.; здесь: Thm.10.4</ref>
Это задача [[Класс P|Р-класса]],так как XOR-SAT формулу можно рассматривать как систему линейных уравнений по модулю 2,которая ,в свою очередь, может быть решена за <tex>O(n^3)</tex> [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 методом Гаусса].Такое представление возможно на основе [https://en.wikipedia.org/wiki/Boolean_algebra_(structure)#Boolean_rings связи между Булевой алгеброй и Булевым кольцом] и тот факт,что арифметика по модулю 2 образует [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 конечное поле].
==Решения XOR-SAT задачи методом Гаусса==
{| align="center" class="wikitable collapsible collapsed" style="text-align:left; margin: 1em"
|-
! Solving an XOR-SAT example<BR>by Gaussian elimination
|-
|
{| align="left" class="collapsible collapsed" style="text-align:left"
|-
! Given formula
|-
| ("⊕" means XOR, the {{color|#ff8080|red clause}} is optional)
|-
| (''a''⊕''c''⊕''d'') ∧ (''b''⊕¬''c''⊕''d'') ∧ (''a''⊕''b''⊕¬''d'') ∧ (''a''⊕¬''b''⊕¬''c'') {{color|#ff8080|∧ (¬''a''⊕''b''⊕''c'')}}
|}
|-
|
{| align="left" class="collapsible collapsed" style="text-align:left"
|-
! colspan="9" | Equation system
|-
| colspan="9" | ("1" means TRUE, "0" means FALSE)
|-
| colspan="9" | Each clause leads to one equation.
|-
| || ''a'' || ⊕ || || ''c'' || ⊕ || || ''d'' || = 1
|-
| || ''b'' || ⊕ || ¬ || ''c'' || ⊕ || || ''d'' || = 1
|-
| || ''a'' || ⊕ || || ''b'' || ⊕ || ¬ || ''d'' || = 1
|-
| || ''a'' || ⊕ || ¬ || ''b'' || ⊕ || ¬ || ''c'' || = 1
|-
| {{color|#ff8080|¬}} || {{color|#ff8080|''a''}} || {{color|#ff8080|⊕}} || || {{color|#ff8080|''b''}} || {{color|#ff8080|⊕}} || || {{color|#ff8080|''c''}} || {{color|#ff8080| ≃ 1}}
|}
|-
|
{| align="left" class="collapsible collapsed" style="text-align:left"
|-
! colspan="6" | Normalized equation system
|-
| colspan="6" | 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'''
|-
| {{color|#ff8080|''a''}} || {{color|#ff8080|⊕}} || {{color|#ff8080|''b''}} || {{color|#ff8080|⊕}} || {{color|#ff8080|''c''}} || {{color|#ff8080| ≃ '''0'''}}
|-
| colspan="6" | (If the {{color|#ff8080|red equation}} is present, {{color|#ff8080|it}} contradicts
|-
| colspan="6" | the last black one, so the system is unsolvable.
|-
| colspan="6" | Therefore, Gauss' algorithm is
|-
| colspan="6" | used only for the black equations.)
|}
|-
|
{| align="left" class="collapsible collapsed" style="text-align:left"
|-
! colspan="6" | 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
|}
|-
|
{| align="left" class="collapsible collapsed" style="text-align:left"
|-
! colspan="6" |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
|}
|-
|
{| align="left" class="collapsible collapsed" style="text-align:left"
|-
! colspan="6" | 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
|-
|}
|-
|
{| align="left" class="collapsible collapsed" style="text-align:left"
|-
! Solution:
|-
| If the {{color|#ff8080|red clause}} is present: || Unsolvable
|-
| Else: || ''a'' = 0 = FALSE
|-
| || ''b'' = 1 = TRUE
|-
| || ''c'' = 0 = FALSE
|-
| || ''d'' = 1 = TRUE
|-
| colspan="2" | '''As a consequence:'''
|-
| colspan="2" | ''R''(''a'',''c'',''d'') ∧ ''R''(''b'',¬''c'',''d'') ∧ ''R''(''a'',''b'',¬''d'') ∧ ''R''(''a'',¬''b'',¬''c'') {{color|#ff8080|∧ ''R''(¬''a'',''b'',''c'')}}
|-
| colspan="2" | is not 1-in-3-satisfiable,
|-
| colspan="2" | while (''a''∨''c''∨''d'') ∧ (''b''∨¬''c''∨''d'') ∧ (''a''∨''b''∨¬''d'') ∧ (''a''∨¬''b''∨¬''c'')
|-
| colspan="2" | is 3-satisfiable with ''a''=''c''=FALSE and ''b''=''d''=TRUE.
|}
|}
==Вычислительная сложность==
[[Файл:Булева выполнимость.png|400px|thumb|down|Формула с 2-мя дизъюнктами может быть неудовлетворена(красный),3-SAT(зелёный),XOR-3-SAT(синий) ,ИЛИ/И 1-in-3-SAT, в зависимости от количества переменных со значением TRUE в 1-м (горизонтальном) и втором (вертикальном) дизъюнкте.]]
Поскольку a XOR b XOR c принимает значение TRUE,если и только если 1 из 3 переменных {a,b,c} принимает значение TRUE,каждое решение в 1-in-3-SAT задачи для данной КНФ-формулы является также решением XOR-3-SAT задачи,и ,в свою очередь,обратное также верно. Как следствие, для каждой КНФ-формулы, можно решить XOR-3-SAT -задачу и на основании результатов сделать вывод, что либо 3-SAT-задача решаема или, что 1-in-3-SAT-задача нерешаема.
При условии ,что P- и NP-классы не равны,ни 2-,ни Хорн-,ни XOR-SAT не являются задачи [[Класс NP|NP-класса]],в отличии от SAT.
== См. также ==
*[[Специальные формы КНФ]]
*[[2SAT]]
*[[3CNFSAT | NP-полнота задачи о выполнимости булевой формулы в форме 3-КНФ]]
== Примечания ==
<references/>
== Источники информации ==
*[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.
[[Категория: Дискретная математика и алгоритмы]]
[[Категория: Булевы функции ]]
|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> операторы.(Формально, обобщенная КНФ с тернарным булевым оператором R работает только если 1 или 3 переменные дают TRUE в своих аргументах. Дизъюнкт,имеющие более 3 переменных могут быть преобразованы в сочетании с формулой преобразования с сохранением выполнимости булевой функции(ссылка на книгу ниже), т. е. XOR-SAT может быть снижена до XOR-3-SAT)<ref>Alfred V. Aho; John E. Hopcroft; Jeffrey D. Ullman (1974). The Design and Analysis of Computer Algorithms. Addison-Wesley.; здесь: Thm.10.4</ref>
Это задача [[Класс P|Р-класса]],так как XOR-SAT формулу можно рассматривать как систему линейных уравнений по модулю 2,которая ,в свою очередь, может быть решена за <tex>O(n^3)</tex> [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 методом Гаусса].Такое представление возможно на основе [https://en.wikipedia.org/wiki/Boolean_algebra_(structure)#Boolean_rings связи между Булевой алгеброй и Булевым кольцом] и тот факт,что арифметика по модулю 2 образует [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 конечное поле].
==Решения XOR-SAT задачи методом Гаусса==
{| align="center" class="wikitable collapsible collapsed" style="text-align:left; margin: 1em"
|-
! Solving an XOR-SAT example<BR>by Gaussian elimination
|-
|
{| align="left" class="collapsible collapsed" style="text-align:left"
|-
! Given formula
|-
| ("⊕" means XOR, the {{color|#ff8080|red clause}} is optional)
|-
| (''a''⊕''c''⊕''d'') ∧ (''b''⊕¬''c''⊕''d'') ∧ (''a''⊕''b''⊕¬''d'') ∧ (''a''⊕¬''b''⊕¬''c'') {{color|#ff8080|∧ (¬''a''⊕''b''⊕''c'')}}
|}
|-
|
{| align="left" class="collapsible collapsed" style="text-align:left"
|-
! colspan="9" | Equation system
|-
| colspan="9" | ("1" means TRUE, "0" means FALSE)
|-
| colspan="9" | Each clause leads to one equation.
|-
| || ''a'' || ⊕ || || ''c'' || ⊕ || || ''d'' || = 1
|-
| || ''b'' || ⊕ || ¬ || ''c'' || ⊕ || || ''d'' || = 1
|-
| || ''a'' || ⊕ || || ''b'' || ⊕ || ¬ || ''d'' || = 1
|-
| || ''a'' || ⊕ || ¬ || ''b'' || ⊕ || ¬ || ''c'' || = 1
|-
| {{color|#ff8080|¬}} || {{color|#ff8080|''a''}} || {{color|#ff8080|⊕}} || || {{color|#ff8080|''b''}} || {{color|#ff8080|⊕}} || || {{color|#ff8080|''c''}} || {{color|#ff8080| ≃ 1}}
|}
|-
|
{| align="left" class="collapsible collapsed" style="text-align:left"
|-
! colspan="6" | Normalized equation system
|-
| colspan="6" | 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'''
|-
| {{color|#ff8080|''a''}} || {{color|#ff8080|⊕}} || {{color|#ff8080|''b''}} || {{color|#ff8080|⊕}} || {{color|#ff8080|''c''}} || {{color|#ff8080| ≃ '''0'''}}
|-
| colspan="6" | (If the {{color|#ff8080|red equation}} is present, {{color|#ff8080|it}} contradicts
|-
| colspan="6" | the last black one, so the system is unsolvable.
|-
| colspan="6" | Therefore, Gauss' algorithm is
|-
| colspan="6" | used only for the black equations.)
|}
|-
|
{| align="left" class="collapsible collapsed" style="text-align:left"
|-
! colspan="6" | 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
|}
|-
|
{| align="left" class="collapsible collapsed" style="text-align:left"
|-
! colspan="6" |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
|}
|-
|
{| align="left" class="collapsible collapsed" style="text-align:left"
|-
! colspan="6" | 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
|-
|}
|-
|
{| align="left" class="collapsible collapsed" style="text-align:left"
|-
! Solution:
|-
| If the {{color|#ff8080|red clause}} is present: || Unsolvable
|-
| Else: || ''a'' = 0 = FALSE
|-
| || ''b'' = 1 = TRUE
|-
| || ''c'' = 0 = FALSE
|-
| || ''d'' = 1 = TRUE
|-
| colspan="2" | '''As a consequence:'''
|-
| colspan="2" | ''R''(''a'',''c'',''d'') ∧ ''R''(''b'',¬''c'',''d'') ∧ ''R''(''a'',''b'',¬''d'') ∧ ''R''(''a'',¬''b'',¬''c'') {{color|#ff8080|∧ ''R''(¬''a'',''b'',''c'')}}
|-
| colspan="2" | is not 1-in-3-satisfiable,
|-
| colspan="2" | while (''a''∨''c''∨''d'') ∧ (''b''∨¬''c''∨''d'') ∧ (''a''∨''b''∨¬''d'') ∧ (''a''∨¬''b''∨¬''c'')
|-
| colspan="2" | is 3-satisfiable with ''a''=''c''=FALSE and ''b''=''d''=TRUE.
|}
|}
==Вычислительная сложность==
[[Файл:Булева выполнимость.png|400px|thumb|down|Формула с 2-мя дизъюнктами может быть неудовлетворена(красный),3-SAT(зелёный),XOR-3-SAT(синий) ,ИЛИ/И 1-in-3-SAT, в зависимости от количества переменных со значением TRUE в 1-м (горизонтальном) и втором (вертикальном) дизъюнкте.]]
Поскольку a XOR b XOR c принимает значение TRUE,если и только если 1 из 3 переменных {a,b,c} принимает значение TRUE,каждое решение в 1-in-3-SAT задачи для данной КНФ-формулы является также решением XOR-3-SAT задачи,и ,в свою очередь,обратное также верно. Как следствие, для каждой КНФ-формулы, можно решить XOR-3-SAT -задачу и на основании результатов сделать вывод, что либо 3-SAT-задача решаема или, что 1-in-3-SAT-задача нерешаема.
При условии ,что P- и NP-классы не равны,ни 2-,ни Хорн-,ни XOR-SAT не являются задачи [[Класс NP|NP-класса]],в отличии от SAT.
== См. также ==
*[[Специальные формы КНФ]]
*[[2SAT]]
*[[3CNFSAT | NP-полнота задачи о выполнимости булевой формулы в форме 3-КНФ]]
== Примечания ==
<references/>
== Источники информации ==
*[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.
[[Категория: Дискретная математика и алгоритмы]]
[[Категория: Булевы функции ]]
