Изменения

Одним из особых случаев <b><tex>\mathrm {SAT}</tex></b> является класс задач, где каждый конъюнкт содержит операции <tex>\oplus</tex> (т. е. исключающее или), а не (обычные) <tex>\lor</tex> операторы.(Формально, обобщенная КНФ с тернарным булевым оператором R работает только если 1 или 3 переменные дают <b><tex>\mathrm {TRUE}</tex></b> в своих аргументах. Конъюнкты,имеющие более 3 переменных могут быть преобразованы в сочетании с формулой преобразования с сохранением выполнимости булевой функции(ссылка на книгу ниже), т. е. <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.''The Design and Analysis of Computer Algorithms. Addison-Wesley.; здесь: Thm.10.4,1974.</ref>