|
|
Строка 1: |
Строка 1: |
− | {{Задача
| + | ХУЙ |
− | |definition = <b><tex>\mathrm {XORSAT}</tex></b> (англ. ''XOR-satisfiability'') выполнимость функции — задача распределения аргументов в булевой [[КНФ|КНФ]] функции, записанной в виде XOR-КНФ, таким образом, чтобы результат данной функции был равен <tex> 1 </tex>.
| |
− | }}
| |
− | | |
− | | |
− | == Описание ==
| |
− | | |
− | Одним из самых главных особых случаев <tex>\mathrm {SAT}</tex> является класс 8 В задач, где каждый конъюнкт содержит операции <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>.
| |
− | | |
− | ==Пример решения XORSAT==
| |
− | ===Пример===
| |
− | <font color='red'>Красные пункты</font> могут быть добавлены для возможности представления КНФ-функции в виде <tex>\mathrm {XOR}</tex>-<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)</tex>
| |
− | ! style="background: #ffdddd;" |<tex> \land (\neg a \oplus b \oplus c) </tex>
| |
− | |}
| |
− | {| class="wikitable"
| |
− | |+
| |
− | !colspan="2"|Решение XOR-SAT задачи методом Гаусса
| |
− | |-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>\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>
| |
− | !Используя свойства Булевых [[Определение кольца, подкольца, изоморфизмы колец|колец]]
| |
− | (<tex>\neg x=1 \oplus x</tex>, <tex>x \oplus x=1</tex>),<br>
| |
− | избавимся от отрицаний в нашей системе
| |
− | |-align="center"
| |
− | !
| |
− | <center>
| |
− | {| class="wikitable" align="center" style="color: blue; background-color:#ffffcc;" cellpadding="10"
| |
− | |+
| |
− | !colspan="6"|Матрица соответствующих коэффициентов
| |
− | |-align="center"
| |
− | !class="dark"| <tex>a</tex>
| |
− | !class="dark"| <tex>b</tex>
| |
− | !class="dark"| <tex>c</tex>
| |
− | !class="dark"| <tex>d</tex>
| |
− | !class="green" style="font-weight:normal" style="background: #ddffdd;"|
| |
− | |Строка
| |
− | |-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>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>
| |
− | !Составим матрицу по следующему правилу:
| |
− | Если переменная присутствовала в данном конъюнкте<br>
| |
− | ставим в ячейку <tex>1</tex>, иначе <tex>0</tex>
| |
− | |-align="center"
| |
− | !
| |
− | <center>
| |
− | {| class="wikitable" align="center" style="color: blue; background-color:#ffffcc;" cellpadding="10"
| |
− | |+
| |
− | !colspan="6"|Преобразования, чтобы сформировать
| |
− | верхнюю треугольную матрицу
| |
− | |-align="center"
| |
− | !class="dark"| <tex>a</tex>
| |
− | !class="dark"| <tex>b</tex>
| |
− | !class="dark"| <tex>c</tex>
| |
− | !class="dark"| <tex>d</tex>
| |
− | !class="green" style="font-weight:normal" style="background: #ddffdd;"|
| |
− | |Операция
| |
− | |-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>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>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="center"
| |
− | !
| |
− | <center>
| |
− | {| class="wikitable" align="center" style="color: blue; background-color:#ffffcc;" cellpadding="10"
| |
− | |+
| |
− | |-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>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>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"| <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>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> при одинаковых аргументах,
| |
− | применим её для строк <tex>A,\ C=E</tex> и <tex>A,\ D=F</tex>,<br>
| |
− | чтобы получить <tex>0</tex> в <tex>1</tex>-м столбце.
| |
− | |-align="center"
| |
− | !
| |
− | <center>
| |
− | {| class="wikitable" align="center" style="color: blue; background-color:#ffffcc;" cellpadding="10"
| |
− | |+
| |
− | |-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>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>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>1</tex>
| |
− | !class="green" style="font-weight:normal" style="background: #ddffdd;"| <tex>1</tex>
| |
− | | <tex>G=F \oplus 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>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=B \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>
| |
− | {| class="wikitable" align="center" style="color: blue; background-color:#ffffcc;" cellpadding="10"
| |
− | |+
| |
− | !colspan="6"|Преобразования, чтобы сформировать
| |
− | диагональную матрицу
| |
− | |-align="center"
| |
− | !class="dark"| <tex>a</tex>
| |
− | !class="dark"| <tex>b</tex>
| |
− | !class="dark"| <tex>c</tex>
| |
− | !class="dark"| <tex>d</tex>
| |
− | !class="green" style="font-weight:normal" style="background: #ddffdd;"|
| |
− | |Операция
| |
− | |-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 \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>
| |
− | !class="green" style="font-weight:normal" style="background: #ddffdd;"| <tex>0</tex>
| |
− | | <tex>J=G \oplus H</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>
| |
− | |}
| |
− | </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>
| |
− | {| class="wikitable" align="center" style="color: blue; background-color:#ffffcc;" cellpadding="10"
| |
− | |+
| |
− | |-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>0</tex>
| |
− | !class="dark" style="font-weight:normal"| <tex>0</tex>
| |
− | !class="green" style="font-weight:normal" style="background: #ddffdd;"| <tex>0</tex>
| |
− | | <tex>K=I \oplus J</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>0</tex>
| |
− | !class="dark" style="font-weight:normal"| <tex>0</tex>
| |
− | !class="green" style="font-weight:normal" style="background: #ddffdd;"| <tex>1</tex>
| |
− | | <tex>L=E \oplus 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>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|Формула с <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>-м (горизонтальном) и втором (вертикальном) конъюнкте.]]
| |
− | Поскольку <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>
| |
− | Как следствие, для каждой КНФ-формулы, можно решить <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>.
| |
− | | |
− | == См. также ==
| |
− | | |
− | *[[Специальные формы КНФ]]
| |
− | *[[2SAT]]
| |
− | *[[3CNFSAT | NP-полнота задачи о выполнимости булевой формулы в форме 3-КНФ]]
| |
− | | |
− | == Примечания ==
| |
− | <references/>
| |
− | | |
− | == Источники информации ==
| |
− | | |
− | *[https://en.wikipedia.org/wiki/Boolean_satisfiability_problem Википедия — Boolean satisfiability problem]
| |
− | * ''Cook, Stephen A.''Proceedings of the 3rd Annual ACM Symposium on Theory of Computing: 151–158, 1971.
| |
− | | |
− | [[Категория: Дискретная математика и алгоритмы]]
| |
− | | |
− | [[Категория: Булевы функции]]
| |