Изменения

Выполним [[сведение по Карпу ]] задачи <tex>SAT</tex> к задаче <tex>CNFSAT</tex>. Для этого необходимо построить функцию <tex>f</tex>, вычислимую за полиномиальное время от длины входа, которая выполняла бы преобразование <tex>\phi \to \omega</tex>, где <tex>\omega</tex> в КНФ. Заметим, что в общем случае время построения эквивалентной формулы в форме КНФ может оказаться больше полиномиального. В частности, длина формулы может вырасти экспоненциально, и тогда время порождения тоже экспоненциально вырастет. Однако нам достаточно предъявить формулу <tex>\omega</tex>, которая будет выполнима тогда и только тогда, когда выполнима исходная формула <tex>\phi</tex>. При этом формулы могут оказаться не эквивалентными, ввиду, например, добавления новых переменных.