Изменения

<tex>\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)</tex> 

// Если Cn(фи)=0 то для любого x (для любого тут можем использовать) фи(х)=0Если Cn(фи)=1 то либо фи(ч1=0) принадлежит сат либо фи(х1=1) принадлежит сат тут не N а длина фи Вот когда подставим x1=0 нужно будет использовать(получится более короткая формула) и используем для проверки логическую схему более короткую . Если она выдает 1 то мы опять подставляем либо 0 либо 1 и так далее. Это правильная проверка причем за полином

Если <tex>C</tex> решает <tex>SAT</tex> то все хорошо. Если нет, если нет то зафиксируем формулу которую он не решает. Если на этой формуле выдаст 0 , а должна выдать 1 , то вот эту получается что не удовлетворяет первую часть не удолветворяет и тут не будет работать, если наоборот выдаст 1 а на самом деле формула не удавлетворима то ни эта ни эта обе скобки работать не будет работатьбудут.

Рассмотрим минимальную схему которая неправильна, тогда на той формуле, на которой эта схема неправильна по . По предположению , что все более короткие формулы правильны,эта формула распознается схемами с меньшим числом входов, поэтому и . Поэтому эта и эта будут 0 и мы не узнаем набор схем. Можно попробовать развернуть формулу до конца. Видимо это будет выглядеть так