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

Материал из Викиконспекты
Перейти к: навигация, поиск
м (Решения XOR-SAT задачи методом Гаусса)
м (rollbackEdits.php mass rollback)
 
(не показано 69 промежуточных версий 5 участников)
Строка 1: Строка 1:
 
{{Задача
 
{{Задача
|definition = <b><tex>\mathrm {XORSAT}</tex></b> (XOR-satisfiability) выполнимость функции — задача распределения аргументов в булевой [[КНФ|КНФ]] функции, записанной в виде XOR-КНФ, таким образом, чтобы результат данной функции был равен <tex> 1 </tex>.
+
|definition = <b><tex>\mathrm {XORSAT}</tex></b> (англ. ''XOR-satisfiability'') выполнимость функции — задача распределения аргументов в булевой [[КНФ|КНФ]] функции, записанной в виде XOR-КНФ, таким образом, чтобы результат данной функции был равен <tex> 1 </tex>.
 
}}
 
}}
  
Строка 6: Строка 6:
 
== Описание ==
 
== Описание ==
  
Одним из особых случаев <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>
+
Одним из особых случаев <tex>\mathrm {SAT}</tex> является класс задач, где каждый конъюнкт содержит операции <tex>\oplus</tex> (т. е. исключающее или), а не (обычные) <tex>\lor</tex> операторы.Формально, обобщенная КНФ с тернарным  булевым  оператором <tex> R</tex> работает  только если <tex> 1</tex> или <tex> 3</tex> переменные дают <tex> \mathtt {true}</tex> в своих аргументах. Конъюнкты, имеющие более <tex> 3</tex> переменных могут быть преобразованы в сочетании с формулой преобразования с сохранением выполнимости булевой функции, т. е. <tex>\mathrm {XOR}</tex>-<tex>\mathrm {SAT}</tex> может быть снижена до <tex>\mathrm {XOR}</tex>-<tex>3</tex>-<tex>\mathrm {SAT}</tex><ref>''Alfred V. Aho; John E. Hopcroft; Jeffrey D. Ullman.''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|Р-класса]],так как 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 конечное поле].
+
==Пример решения XORSAT==
 
+
===Пример===
==Решение XOR-SAT задачи методом Гаусса==
+
<font color='red'>Красные пункты</font> могут быть добавлены для возможности представления КНФ-функции в виде <tex>\mathrm {XOR}</tex>-<tex>\mathrm {SAT}</tex>.
 
+
{| class="wikitable"
{| align="center" class="wikitable collapsible collapsed" style="text-align:left; margin: 1em"
+
!<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)</tex>
|-
+
! style="background: #ffdddd;" |<tex> \land (\neg a \oplus  b \oplus c) </tex>
! Solving an XOR-SAT example<BR>by Gaussian elimination
+
|}
|-
+
{| class="wikitable"
|
+
|+
{| align="left" class="collapsible collapsed" style="text-align:left"
+
!colspan="2"|Решение XOR-SAT задачи методом Гаусса
|-
+
|-align="center"
! Given formula
+
!
|-
+
<center>
| ("" means XOR, the {{color|#ff8080|red clause}} is optional)
+
{| class="wikitable" align="center" style="color: blue; background-color:#ffffcc;" cellpadding="10"
|-
+
|+
| (''a''⊕''c''⊕''d'') ∧ (''b''⊕¬''c''⊕''d'') ∧ (''a''⊕''b''⊕¬''d'') ∧ (''a''⊕¬''b''⊕¬''c'') {{color|#ff8080|∧ (¬''a''⊕''b''⊕''c'')}}
+
!colspan="2"|Система уравнений
 +
|-align="center"
 +
!Переменные
 +
|! width="20%" | Значение
 +
|-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>\neg c </tex> <tex>\oplus</tex> <tex> d </tex>
 +
|<tex>=1</tex>
 +
|-align="center"
 +
! <tex> a </tex> <tex>\oplus</tex> <tex>  b </tex> <tex>\oplus</tex> <tex>\neg d </tex>
 +
|<tex>=1</tex>
 +
|-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"
 +
! style="background: #ffdddd;" |<tex> \neg a </tex> <tex>\oplus</tex> <tex>  b </tex>  <tex>\oplus</tex>  <tex> c </tex>
 +
! style="background: #ffdddd;" |<tex> =1 </tex>
 +
|}
 +
</center>
 +
!(«<tex>1</tex>» означает «<tex> \mathtt {true}</tex>», «<tex>0</tex>» означает «<tex> \mathtt {false}</tex>»)
 +
Каждый конъюнкт ведет к одному уравнению.
 +
|-align="center"
 +
!
 +
<center>
 +
{| 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</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 </tex>
 +
|<tex>=1</tex>
 +
|-align="center"
 +
! style="background: #ffdddd;" |<tex> a </tex> <tex>\oplus</tex> <tex>  b </tex>  <tex>\oplus</tex>  <tex> c </tex>
 +
! style="background: #ffdddd;" |<tex> =0 </tex>
 
|}
 
|}
|-
+
</center>
|
+
!Используя свойства Булевых [[Определение кольца, подкольца, изоморфизмы колец|колец]]
{| align="left" class="collapsible collapsed" style="text-align:left"
+
(<tex>\neg x=1 \oplus x</tex>, <tex>x \oplus x=1</tex>),<br>
|-
+
избавимся от отрицаний в нашей системе
! colspan="9" | Equation system
+
|-align="center"
|-
+
!
| colspan="9" | ("1" means TRUE, "0" means FALSE)
+
<center>
|-
+
{| class="wikitable" align="center" style="color: blue; background-color:#ffffcc;" cellpadding="10"
| colspan="9" | Each clause leads to one equation.
+
|+
|-
+
!colspan="6"|Матрица соответствующих коэффициентов
| || ''a'' || ⊕ ||  || ''c'' || ⊕ ||  || ''d'' || = 1
+
|-align="center"
|-
+
!class="dark"| <tex>a</tex>
| || ''b'' || ⊕ || ¬ || ''c'' || ⊕ ||  || ''d'' || = 1
+
!class="dark"| <tex>b</tex>
|-
+
!class="dark"| <tex>c</tex>
| || ''a'' || ⊕ ||  || ''b'' || ⊕ || ¬ || ''d'' || = 1
+
!class="dark"| <tex>d</tex>
|-
+
!class="green" style="font-weight:normal" style="background: #ddffdd;"|
| || ''a'' || ⊕ || ¬ || ''b'' || ⊕ || ¬ || ''c'' || = 1
+
|Строка
|-
+
|-align="center"
| {{color|#ff8080|¬}} || {{color|#ff8080|''a''}} || {{color|#ff8080|⊕}} || || {{color|#ff8080|''b''}} || {{color|#ff8080|⊕}} || || {{color|#ff8080|''c''}} || {{color|#ff8080| ≃ 1}}
+
  !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>1</tex>
 +
  !class="green" style="font-weight:normal" style="background: #ddffdd;"| <tex>1</tex>
 +
| <tex>A</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>1</tex>
 +
  !class="green" style="font-weight:normal" style="background: #ddffdd;"| <tex>0</tex>
 +
| <tex>B</tex>
 +
|-align="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"| <tex>0</tex>
 +
!class="dark" style="font-weight:normal"| <tex>1</tex>
 +
!class="green" style="font-weight:normal" style="background: #ddffdd;"| <tex>0</tex>
 +
| <tex>C</tex>
 +
|-align="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"| <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>D</tex>
 
|}
 
|}
|-
+
</center>
|
+
!Составим матрицу по следующему правилу:
{| align="left" class="collapsible collapsed" style="text-align:left"
+
Если переменная присутствовала в данном конъюнкте<br>
|-
+
ставим в ячейку <tex>1</tex>, иначе <tex>0</tex>
! colspan="6" | Normalized equation system
+
|-align="center"
|-
+
!
| colspan="6" | using properties of [[Boolean rings]] (¬''x''=1⊕''x'', ''x''⊕''x''=0)
+
<center>
|-
+
{| class="wikitable" align="center" style="color: blue; background-color:#ffffcc;" cellpadding="10"
| ''a'' || ⊕ || ''c'' || ⊕ || ''d'' || = '''1'''
+
|+
|-
+
!colspan="6"|Преобразования, чтобы сформировать
| ''b'' || || ''c'' || ⊕ || ''d'' || = '''0'''
+
верхнюю треугольную матрицу
|-
+
|-align="center"
| ''a'' || ⊕ || ''b'' || ⊕ || ''d'' || = '''0'''
+
!class="dark"| <tex>a</tex>
|-
+
!class="dark"| <tex>b</tex>
| ''a'' || ⊕ || ''b'' || ⊕ || ''c'' || = '''1'''
+
!class="dark"| <tex>c</tex>
|-
+
!class="dark"| <tex>d</tex>
| {{color|#ff8080|''a''}} || {{color|#ff8080|⊕}} || {{color|#ff8080|''b''}} || {{color|#ff8080|⊕}} || {{color|#ff8080|''c''}} || {{color|#ff8080| ≃ '''0'''}}
+
!class="green" style="font-weight:normal" style="background: #ddffdd;"|  
|-
+
|Операция
| colspan="6" | (If the {{color|#ff8080|red equation}} is present, {{color|#ff8080|it}} contradicts
+
|-align="center"
|-
+
!class="dark" style="font-weight:normal"| <tex>1</tex>
| colspan="6" | the last black one, so the system is unsolvable.
+
!class="dark" style="font-weight:normal"| <tex>0</tex>
|-
+
!class="dark" style="font-weight:normal"| <tex>1</tex>
| colspan="6" | Therefore, Gauss' algorithm is
+
!class="dark" style="font-weight:normal"| <tex>1</tex>
|-
+
!class="green" style="font-weight:normal" style="background: #ddffdd;"| <tex>1</tex>
| colspan="6" | used only for the black equations.)
+
| <tex>A</tex>
 +
|-align="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"| <tex>0</tex>
 +
!class="dark" style="font-weight:normal"| <tex>1</tex>
 +
!class="green" style="font-weight:normal" style="background: #ddffdd;"| <tex>0</tex>
 +
| <tex>C</tex>
 +
|-align="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"| <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>D</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>1</tex>
 +
!class="green" style="font-weight:normal" style="background: #ddffdd;"| <tex>0</tex>
 +
| <tex>B</tex>
 
|}
 
|}
|-
+
</center>
|
+
!Поменяем местами строки <tex>B,\ C,\ D</tex>,<br>
{| align="left" class="collapsible collapsed" style="text-align:left"
+
чтобы упростить получение верхней треугольной матрицы.
|-
+
|-align="center"
! colspan="6" | Associated coefficient matrix
+
!
|-
+
<center>
| &nbsp;
+
{| class="wikitable" align="center" style="color: blue; background-color:#ffffcc;" cellpadding="10"
|-
+
|+
! ''a'' !! ''b'' !! ''c'' !! ''d'' !!  !! line
+
|-align="center"
|-
+
!class="dark" style="font-weight:normal"| <tex>1</tex>
| &nbsp;
+
!class="dark" style="font-weight:normal"| <tex>0</tex>
|-
+
!class="dark" style="font-weight:normal"| <tex>1</tex>
| 1 || 0 || 1 || 1
+
!class="dark" style="font-weight:normal"| <tex>1</tex>
! 1
+
!class="green" style="font-weight:normal" style="background: #ddffdd;"| <tex>1</tex>
| A
+
| <tex>A</tex>
|-
+
|-align="center"
| 0 || 1 || 1 || 1
+
!class="dark" style="font-weight:normal"| <tex>0</tex>
! 0
+
!class="dark" style="font-weight:normal"| <tex>1</tex>
| B
+
!class="dark" style="font-weight:normal"| <tex>1</tex>
|-
+
!class="dark" style="font-weight:normal"| <tex>0</tex>
| 1 || 1 || 0 || 1
+
!class="green" style="font-weight:normal" style="background: #ddffdd;"| <tex>1</tex>
! 0
+
| <tex>E=C \oplus A</tex>
| C
+
|-align="center"
|-
+
!class="dark" style="font-weight:normal"| <tex>0</tex>
| 1 || 1 || 1 || 0
+
!class="dark" style="font-weight:normal"| <tex>1</tex>
! 1
+
!class="dark" style="font-weight:normal"| <tex>0</tex>
| D
+
!class="dark" style="font-weight:normal"| <tex>1</tex>
 +
!class="green" style="font-weight:normal" style="background: #ddffdd;"| <tex>0</tex>
 +
| <tex>F=D \oplus A</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>1</tex>
 +
!class="green" style="font-weight:normal" style="background: #ddffdd;"| <tex>0</tex>
 +
| <tex>B</tex>
 
|}
 
|}
|-
+
</center>
|
+
!Т.к. операция <tex>\oplus</tex> даёт <tex>0</tex>  при одинаковых аргументах,
{| align="left" class="collapsible collapsed" style="text-align:left"
+
применим её для строк <tex>A,\ C=E</tex> и <tex>A,\ D=F</tex>,<br>
|-
+
чтобы получить <tex>0</tex> в <tex>1</tex>-м столбце.
! colspan="6" |Transforming to echelon form
+
|-align="center"
|-
+
!
| &nbsp;
+
<center>
|-
+
{| class="wikitable" align="center" style="color: blue; background-color:#ffffcc;" cellpadding="10"
! ''a'' !! ''b'' !! ''c'' !! ''d'' !!  !! operation
+
|+
|-
+
|-align="center"
| &nbsp;
+
!class="dark" style="font-weight:normal"| <tex>1</tex>
|-
+
!class="dark" style="font-weight:normal"| <tex>0</tex>
| 1 || 0 || 1 || 1
+
!class="dark" style="font-weight:normal"| <tex>1</tex>
! 1
+
!class="dark" style="font-weight:normal"| <tex>1</tex>
| A
+
!class="green" style="font-weight:normal" style="background: #ddffdd;"| <tex>1</tex>
|-
+
| <tex>A</tex>
| 1 || 1 || 0 || 1
+
|-align="center"
! 0
+
!class="dark" style="font-weight:normal"| <tex>0</tex>
| C
+
!class="dark" style="font-weight:normal"| <tex>1</tex>
|-
+
!class="dark" style="font-weight:normal"| <tex>1</tex>
| 1 || 1 || 1 || 0
+
!class="dark" style="font-weight:normal"| <tex>0</tex>
! 1
+
!class="green" style="font-weight:normal" style="background: #ddffdd;"| <tex>1</tex>
| D
+
| <tex>E</tex>
|-
+
|-align="center"
| 0 || 1 || 1 || 1
+
!class="dark" style="font-weight:normal"| <tex>0</tex>
! 0
+
!class="dark" style="font-weight:normal"| <tex>0</tex>
| B (swapped)
+
!class="dark" style="font-weight:normal"| <tex>1</tex>
|-
+
!class="dark" style="font-weight:normal"| <tex>1</tex>
| &nbsp;
+
!class="green" style="font-weight:normal" style="background: #ddffdd;"| <tex>1</tex>
|-
+
| <tex>G=F \oplus E</tex>
| 1 || 0 || 1 || 1
+
|-align="center"
! 1
+
!class="dark" style="font-weight:normal"| <tex>0</tex>
| A
+
!class="dark" style="font-weight:normal"| <tex>0</tex>
|-
+
!class="dark" style="font-weight:normal"| <tex>0</tex>
| 0 || 1 || 1 || 0
+
!class="dark" style="font-weight:normal"| <tex>1</tex>
! 1
+
!class="green" style="font-weight:normal" style="background: #ddffdd;"| <tex>1</tex>
| E = C⊕A
+
| <tex>H=B \oplus E</tex>
|-
 
| 0 || 1 || 0 || 1
 
! 0
 
| F = D⊕A
 
|-
 
| 0 || 1 || 1 || 1
 
! 0
 
| B
 
|-
 
| &nbsp;
 
|-
 
| 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
 
 
|}
 
|}
|-
+
</center>
|
+
!Теперь применим <tex>\oplus</tex> для строк <tex>E,\ F=G</tex> и <tex>B,\ E=H</tex>,<br>
{| align="left" class="collapsible collapsed" style="text-align:left"
+
чтобы получить <tex>0</tex> в <tex>2</tex>-м и <tex>3</tex>-м столбцах.
|-
+
|-align="center"
! colspan="6" | Transforming to diagonal form
+
!
|-
+
<center>
| &nbsp;
+
{| class="wikitable" align="center" style="color: blue; background-color:#ffffcc;" cellpadding="10"
|-
+
|+
! ''a'' !! ''b'' !! ''c'' !! ''d'' !!  !! operation
+
!colspan="6"|Преобразования, чтобы сформировать
|-
+
диагональную матрицу
| &nbsp;
+
|-align="center"
|-
+
!class="dark"| <tex>a</tex>
| 1 || 0 || 1 || 0
+
!class="dark"| <tex>b</tex>
! 0
+
!class="dark"| <tex>c</tex>
| I = A⊕H
+
!class="dark"| <tex>d</tex>
|-
+
!class="green" style="font-weight:normal" style="background: #ddffdd;"|  
| 0 || 1 || 1 || 0
+
|Операция
! 1
+
|-align="center"
| E
+
!class="dark" style="font-weight:normal"| <tex>1</tex>
|-
+
!class="dark" style="font-weight:normal"| <tex>0</tex>
| 0 || 0 || 1 || 0
+
!class="dark" style="font-weight:normal"| <tex>1</tex>
! 0
+
!class="dark" style="font-weight:normal"| <tex>0</tex>
| J = G⊕H
+
!class="green" style="font-weight:normal" style="background: #ddffdd;"| <tex>0</tex>
|-
+
| <tex>I=A \oplus H</tex>
| 0 || 0 || 0 || 1
+
|-align="center"
! 1
+
!class="dark" style="font-weight:normal"| <tex>0</tex>
| H
+
!class="dark" style="font-weight:normal"| <tex>1</tex>
|-
+
!class="dark" style="font-weight:normal"| <tex>1</tex>
| &nbsp;
+
!class="dark" style="font-weight:normal"| <tex>0</tex>
|-
+
!class="green" style="font-weight:normal" style="background: #ddffdd;"| <tex>1</tex>
| 1 || 0 || 0 || 0
+
| <tex>E</tex>
! 0
+
|-align="center"
| K = I⊕J
+
!class="dark" style="font-weight:normal"| <tex>0</tex>
|-
+
!class="dark" style="font-weight:normal"| <tex>0</tex>
| 0 || 1 || 0 || 0
+
!class="dark" style="font-weight:normal"| <tex>1</tex>
! 1
+
!class="dark" style="font-weight:normal"| <tex>0</tex>
| L = E⊕J
+
!class="green" style="font-weight:normal" style="background: #ddffdd;"| <tex>0</tex>
|-
+
| <tex>J=G \oplus H</tex>
| 0 || 0 || 1 || 0
+
|-align="center"
! 0
+
!class="dark" style="font-weight:normal"| <tex>0</tex>
| J
+
!class="dark" style="font-weight:normal"| <tex>0</tex>
|-
+
!class="dark" style="font-weight:normal"| <tex>0</tex>
| 0 || 0 || 0 || 1
+
!class="dark" style="font-weight:normal"| <tex>1</tex>
! 1
+
!class="green" style="font-weight:normal" style="background: #ddffdd;"| <tex>1</tex>
| H
+
| <tex>H</tex>
|-
 
 
|}
 
|}
|-
+
</center>
|
+
!Чтобы получить основную диагональную матрицу,<br>
{| align="left" class="collapsible collapsed" style="text-align:left"
+
сделаем <tex>\oplus</tex> <tex>A,\ H=I</tex> и <tex>G,\ H=J</tex>,<br>
|-
+
чтобы получить <tex>0</tex> в <tex>4</tex>-м столбце выше диагонали.
! Solution:
+
|-align="center"
|-
+
!
| If the {{color|#ff8080|red clause}} is present: || Unsolvable
+
<center>
|-
+
{| class="wikitable" align="center" style="color: blue; background-color:#ffffcc;" cellpadding="10"
| Else: || ''a'' = 0 = FALSE
+
|+
|-
+
|-align="center"
| || ''b'' = 1 = TRUE
+
!class="dark" style="font-weight:normal"| <tex>1</tex>
|-
+
!class="dark" style="font-weight:normal"| <tex>0</tex>
| || ''c'' = 0 = FALSE
+
!class="dark" style="font-weight:normal"| <tex>0</tex>
|-
+
!class="dark" style="font-weight:normal"| <tex>0</tex>
| || ''d'' = 1 = TRUE
+
!class="green" style="font-weight:normal" style="background: #ddffdd;"| <tex>0</tex>
|-
+
| <tex>K=I \oplus J</tex>
| colspan="2" | '''As a consequence:'''
+
|-align="center"
|-
+
!class="dark" style="font-weight:normal"| <tex>0</tex>
| colspan="2" | ''R''(''a'',''c'',''d'') ∧ ''R''(''b'',¬''c'',''d'') ∧ ''R''(''a'',''b'',¬''d'') ∧ ''R''(''a'',¬''b'',¬''c'') {{color|#ff8080|∧ ''R''(¬''a'',''b'',''c'')}}
+
!class="dark" style="font-weight:normal"| <tex>1</tex>
|-
+
!class="dark" style="font-weight:normal"| <tex>0</tex>
| colspan="2" | is not 1-in-3-satisfiable,
+
!class="dark" style="font-weight:normal"| <tex>0</tex>
|-
+
!class="green" style="font-weight:normal" style="background: #ddffdd;"| <tex>1</tex>
| colspan="2" | while (''a''∨''c''∨''d'') ∧ (''b''∨¬''c''∨''d'') ∧ (''a''∨''b''∨¬''d'') ∧ (''a''∨¬''b''∨¬''c'')
+
| <tex>L=E \oplus J</tex>
|-
+
|-align="center"
| colspan="2" |  is 3-satisfiable with ''a''=''c''=FALSE and ''b''=''d''=TRUE.
+
!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>
 +
!class="green" style="font-weight:normal" style="background: #ddffdd;"| <tex>0</tex>
 +
| <tex>J</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>0</tex>
 +
!class="dark" style="font-weight:normal"| <tex>1</tex>
 +
  !class="green" style="font-weight:normal" style="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|Формула с 2-мя дизъюнктами может быть неудовлетворена(красный),3-SAT(зелёный),XOR-3-SAT(синий) ,ИЛИ/И 1-in-3-SAT, в зависимости от количества переменных со значением TRUE в 1-м (горизонтальном) и втором (вертикальном) дизъюнкте.]]
+
[[Файл:Булева выполнимость.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>, в зависимости от количества переменных со значением <tex> \mathtt {true}</tex> в <tex>1</tex>-м (горизонтальном) и втором (вертикальном) конъюнкте.]]
Поскольку 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-задача нерешаема.
+
Поскольку <tex>a \oplus b \oplus c</tex> принимает значение <tex> \mathtt {true}</tex>, если и только если <tex>1</tex> из <tex>3</tex> переменных <tex>\{a,\ b,\ 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>
При условии ,что P- и NP-классы не равны,ни 2-,ни Хорн-,ни XOR-SAT не являются задачи [[Класс NP|NP-класса]],в отличии от SAT.
+
Как следствие, для каждой КНФ-формулы, можно решить <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>.
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
  
 
== См. также ==
 
== См. также ==
Строка 267: Строка 356:
  
 
*[https://en.wikipedia.org/wiki/Boolean_satisfiability_problem Википедия — Boolean satisfiability problem]
 
*[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.  
+
* ''Cook, Stephen A.''Proceedings of the 3rd Annual ACM Symposium on Theory of Computing: 151–158, 1971.  
  
 
[[Категория: Дискретная математика и алгоритмы]]
 
[[Категория: Дискретная математика и алгоритмы]]
  
[[Категория: Булевы функции ]]
+
[[Категория: Булевы функции]]

Текущая версия на 19:42, 4 сентября 2022

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


Описание

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

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

Пример решения XORSAT

Пример

Красные пункты могут быть добавлены для возможности представления КНФ-функции в виде [math]\mathrm {XOR}[/math]-[math]\mathrm {SAT}[/math].

[math](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)[/math] [math] \land (\neg a \oplus b \oplus c) [/math]
Решение XOR-SAT задачи методом Гаусса
Система уравнений
Переменные Значение
[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] =1 [/math]
[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] 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] =0 [/math]
Используя свойства Булевых колец

([math]\neg x=1 \oplus x[/math], [math]x \oplus x=1[/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]1[/math], иначе [math]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]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]B,\ C,\ 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]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]\oplus[/math] даёт [math]0[/math] при одинаковых аргументах,

применим её для строк [math]A,\ C=E[/math] и [math]A,\ D=F[/math],
чтобы получить [math]0[/math] в [math]1[/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]\oplus[/math] для строк [math]E,\ F=G[/math] и [math]B,\ E=H[/math],

чтобы получить [math]0[/math] в [math]2[/math]-м и [math]3[/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]\oplus[/math] [math]A,\ H=I[/math] и [math]G,\ H=J[/math],
чтобы получить [math]0[/math] в [math]4[/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]\oplus[/math] [math]I,\ J=K[/math] и [math]E,\ J=L[/math],

потому что они отличаются в [math]1[/math]-м и [math]2[/math]-м столбцах.

Решение

Если красный пункт присутствует: Решений нет
Иначе:
[math]a=0=\mathtt {false}[/math]
[math]b=1=\mathtt {true}[/math]
[math]c=0=\mathtt {false}[/math]
[math]d=1=\mathtt {true}[/math]

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

Формула с [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] не являются задачи [math]\mathrm {NP}[/math]-класса, в отличии от [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. Конечное поле

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