1632
правки
Изменения
м
# * <tex> x_i \to x_i</tex>;# * <tex> \lnot x \varphi \to 1 - xA_\varphi</tex>;# * <tex>\Phi varphi \land \Psi psi \to A_\Phi varphi \cdot A_\Psipsi</tex>;# * <tex>\Phi varphi \lor \Psi psi \to 1 - (1 - A_\Phivarphi) \cdot (1 - A_\Psipsi)</tex>.; Заметим, что длина формулы при этом возрастёт не более<tex>|A_\phi| \le C |\phi|</tex> , чем в константу разгде <tex>C</tex> {{---}} некоторая константа.
rollbackEdits.php mass rollback
Введём понятие арифметизации булевых формул. Пусть нам дана формула <tex>\phi(x_1 \ldots x_m)</tex>. Сделаем следующие преобразования и получим формулу <tex>A_\phi(x_1, x_2, \ldots, x_m)</tex>:
{{Лемма
|about=1
|statement=<tex>\phi(x_1 \ldots x_m) = A_\phi(x_1, \ldots, x_m)</tex>.
|proof=Непосредственно следует из построения.
}}
Для арифметизации булевых формул с кванторами добавим еще два правила преобразования:
* <tex>\exists x \varphi(x) \to \sum\limits_{x=0}^{1} A_\varphi(x)</tex>;
* <tex>\forall x \varphi(x) \to \prod\limits_{x=0}^{1} A_\varphi(x)</tex>.
Будем обозначать через <tex>Q_i</tex> квантор, связывающий переменную <tex>x_i</tex>. Через <tex>R_i</tex> будем обозначать операцию, в которую преобразуется квантор <tex>Q_i</tex> в процессе арифметизации.
Заметим, что любую булеву формулу можно привести к виду <tex>Q_1 \ldots Q_m \phi(x_1, \ldots, x_m)</tex>, где <tex>\phi</tex> {{---}} формула, не содержащая кванторов. Кроме того, в процессе арифметизации <tex>Q_1 \ldots Q_m \phi(x_1, \ldots, x_m)</tex> переходит в <tex>R_1 \ldots R_m A_\phi(x_1, \ldots, x_m)</tex>. Поэтому далее будем рассматривать только формулы, которые имеют вид, указанный выше.
{{Лемма
|about=2
|statement=
Пусть <tex>Q_1 \ldots Q_m \phi(x_1, \ldots, x_m)</tex> {{---}} булева формула с кванторами, переходящая в процессе арифметизации в <tex>s = R_1 \ldots R_m A_\phi(x_1, \ldots, x_m)</tex>.
<tex>c_1, \ldots, c_m</tex> {{---}} двоичные константы.
Обозначим через <tex>A_i(x_{i+1}) = R_{i+2} \ldots R_m A_\phi(c_1, \ldots, c_i, x_{i+1}, \ldots, x_m)</tex>, где <tex>0 \le i \le m - 1</tex>. Тогда:
#
##Если <tex>R_1 = \sum</tex>, то <tex>A_0(0) + A_0(1) = s</tex>;
##Если <tex>R_1 = \prod</tex>, то <tex>A_0(0) \cdot A_0(1) = s</tex>.
# <tex>\forall i : 1 \le i \le m - 1</tex>
##Если <tex>R_{i+1} = \sum</tex>, то <tex> A_i(0) + A_i(1) = A_{i-1}(c_i)</tex>;
##Если <tex>R_{i+1} = \prod</tex>, то <tex>A_i(0) \cdot A_i(1) = A_{i-1}(c_i)</tex>.
|proof=
Докажем пункты 1.1 и 2.1. Для остальных пунктов доказательство аналогично.
1.1. <tex>s=\sum\limits_{x_1 = 0}^{1}R_2\ldots R_m(x_1, x_2, \ldots, x_m)=R_2 \ldots R_m</tex><tex>(0, x_2, \ldots, x_m) + R_2 \ldots R_m(1, x_2, \ldots, x_m)=A_0(0) + A_0(1)</tex>.
2.1. <tex>A_{i-1}(c_i)=\sum\limits_{x_{i+1} = 0}^{1}R_{i+2}\ldots R_m</tex><tex>(c_1, \ldots, c_{i-1}, c_i, x_{i+1}, \ldots x_m)=R_{i+2} \ldots R_m</tex><tex>(c_1, \ldots, c_i, 0, x_{i+2}, \ldots, x_m) + R_{i+2} \ldots R_m</tex><tex>(c_1, \ldots, c_i, 1, x_{i+2}, \ldots, x_m)=A_i(0) + A_i(1)</tex>.
}}
{{Определение
|definition=
Оператором линеаризации будем называть оператор <tex>L_{i}A(x_i)=(1-x_i) \cdot A</tex><tex>(0)+x_i \cdot A(1)</tex>.
}}
Заметим, что оператор линеаризации уменьшает степень <tex>x_i</tex> до единицы, при этом полученная формула эквивалентна исходной. Кроме того, если дано выражение <tex>R_1 \ldots R_m A_\phi(x_1, \ldots, x_m)</tex>, то <tex>L_{i}</tex> можно вставить в список <tex>R_1,\ldots,R_m</tex> в любое место, после операции <tex>R_i</tex> (для того, чтобы выражение, на которое действует оператор, было функцией от <tex>x_i</tex>). При этом значение выражения не изменится. Операторы <tex>L_i</tex> и <tex>L_j</tex> можно вставлять в выражение независимо друг от друга для любых <tex>1 \le i, j \le m</tex>. Для оператора линеаризации можно сформулировать лемму, аналогичную лемме (2).
{{Лемма
|about=3
|statement=
Пусть <tex>Q_1 \ldots Q_m \phi(x_1, \ldots, x_m)</tex> {{---}} булева формула с кванторами, переходящая в процессе арифметизации в <tex>s = R_1 \ldots R_m A_\phi(x_1, \ldots, x_m)=R_1 \ldots R_{i+1} L_j R_{i+2}\ldots R_m A_\phi(x_1, \ldots, x_m)</tex>, <tex>j < i + 2</tex>.
<tex>c_1, \ldots, c_m</tex> {{---}} двоичные константы.
<tex>A_{i}'(x_1,\ldots,x_{i+1}) = L_j R_{i+2} \ldots R_m A_\phi(x_1, \ldots, x_m)</tex>
<tex>A_{i}(x_1,\ldots,x_{i+1}) = R_{i+2} \ldots R_m A_\phi(x_1, \ldots, x_m)</tex>
Тогда
<tex>A_i'(c_1,\ldots,c_{i+1}) = (1-c_j) \cdot A_i</tex><tex>(c_1,\ldots,c_{j-1},0,c_{j+1},\ldots,c_{i+1}) + c_j \cdot A_i(c_1,\ldots,c_{j-1},1,c_{j+1},\ldots,c_{i+1})</tex>.
}}
