Изменения

Воспользуемся самосведением <tex>SAT</tex>: <tex>L=\{x|\exists{C1,C2,..,Cn} \forall{y} C_n(f(<x,y>))=1\}</tex>, где - <tex>C1,C2,..,Cn</tex> набор логических схем для <tex>SAT</tex>.

Внутри будем проверять используемый набор

<math>\forall{\varphi{}} (C_{|\varphi{}|}(\varphi{})=0 \Rightarrow \forall{x} \varphi(x)=0) (C_{|\varphi{}|}(\varphi{})=1 \Rightarrow \varphi{}|_{x_1=0} \in SAT или \varphi{}|_{x_1=1} \in SAT)</math>

// Если Cn(фи)=0 то для любого x (для любого тут можем использовать) фи(х)=0

Если Cn(фи)=1 то либо фи(ч1=0) принадлежит сат либо фи(х1=1) принадлежит сат тут не N а длина фи