Изменения
Нет описания правки
* <tex>\lnot x \to 1-X</tex>
* <tex>x \land y \to XY</tex>
* <tex>x \lor y \to X+Y-XY = 1-(1-X)(1-Y)</tex>* <tex>\exists x \varphi(x) \to \sum_sum\limits_{X=0}^{1} A_\varPhivarphi(X)</tex>* <tex>\forall x \varphi(x) \to \prod_prod\limits_{X=0}^{1} A_\varPhivarphi(X)</tex>
Результат этого выражения будет ненулевым в том и только в том случае, если исходная формула была истина.
Рассмотрим пример:
<tex>\varphi=\forall x_1 \forall x_2 \cdots \forall x_{k-1} \exists x_k (x_k \lor \lnot x_k)</tex>
<tex>A_\varphi = \prod\limits_{X_1=0}^{1}\prod\limits_{X_2=0}^{1}\cdots \prod\limits_{X_{k-1}=0}^{1}\sum\limits_{X_k=0}^1(1-X_k(1-X_k)) = 2^{2^{(k-1)}}</tex>
Для записи этого числа нужно <tex>2^{(k-1)}</tex> бит. Если <tex>k \gg \log|\varphi|</tex>, его невозможно передать за полиномиальное относительно длины исходной формулы время.
