Изменения
Нет описания правки
Внутри будем проверять используемый набор
<tex>\forall{\varphi{}} (C_{|\varphi{}|}(\varphi{})=0 \Rightarrow \forall{x} \varphi{}(x)=0)\@@eqno (1)
\vee{}</tex>
<tex>(C_{|\varphi{}|}(\varphi{})=1 \Rightarrow \varphi{}|_{x_1=0} \in SAT или \varphi{}|_{x_1=1} \in SAT)\label{f2}</tex>
Вот когда подставим x1=0 нужно будет использовать(получится более короткая формула) и используем для проверки логическую схему более короткую . Если она выдает 1 то мы опять подставляем либо 0 либо 1 и так далее. Это правильная проверка причем за полином
Если <tex>C</tex> решает <tex>SAT</tex> то все хорошо. Если нет, то зафиксируем формулу <tex>\varphi{}_0</tex>, которую он не решает. Если на этой формуле выдаст 0, а должна выдать 1, то получается что не удовлетворяет первую часть <tex>(\ref{f1})</tex>предыдущего выражения и , значит, не будет работать, если . Если наоборот выдаст 1 а на самом деле формула не удавлетворима то обе скобки не выполнятся и опять формула работать не будутбудет.
Рассмотрим минимальную неправильную схему которая неправильна, тогда . Тогда на той формуле, на которой эта схема неправильна. По , по предположению, что все более короткие формулы правильны,эта формула распознается схемами с меньшим числом входов. Поэтому эта и эта будут 0 и мы не узнаем набор схем. Можно попробовать развернуть формулу до конца. Видимо это будет выглядеть так
<tex> \forall{\varphi{}}: |\varphi{}|=m \forall{x_1}..\forall{x_m} если C_m(\varphi{})=0 \Rightarrow \varphi{(x_1)}=0 иначе C_{m-1}(\varphi|_{x_1=0})=0 \Rightarrow \varphi|_{x_1=0}(x_2)=0</tex>
