Арифметизация булевых формул с кванторами

Введём понятие арифметизации булевых формул. Пусть нам дана формула [math]\phi(x_1 \ldots x_m)[/math]. Сделаем следующие преобразования и получим формулу [math]A_\phi(x_1, x_2, \ldots, x_m)[/math]:

• [math]x_i \to x_i[/math];
• [math]\lnot x \to 1 - x[/math];
• [math]\varphi \land \psi \to A_\varphi \cdot A_\psi[/math];
• [math]\varphi \lor \psi \to 1 - (1 - A_\varphi) \cdot (1 - A_\psi)[/math];

Заметим, что [math]|A_\phi| \le C |\phi|[/math] , где [math]C[/math] — некоторая константа.

Лемма (1):

[math]\phi(x_1 \ldots x_m) = A_\phi(x_1, \ldots, x_m)[/math].

Доказательство:

[math]\triangleright[/math]

proof

[math]\triangleleft[/math]

Для арифметизации булевых формул с кванторами добавим еще два правила преобразования:

• [math]\exists x \varphi(x) \to \sum\limits_{x=0}^{1} A_\varphi(x)[/math];
• [math]\forall x \varphi(x) \to \prod\limits_{x=0}^{1} A_\varphi(x)[/math].

Будем обозначать через [math]Q_i[/math] квантор, связывающий переменную [math]x_i[/math]. Через [math]R_i[/math] будем обозначать операцию, в которую преобразуется квантор [math]Q_i[/math] в процессе арифметизации.

Заметим, что любую булеву формулу можно привести к виду [math]Q_1 \ldots Q_m \phi(x_1, \ldots, x_m)[/math], где [math]\phi[/math] — формула, не содержащая кванторов. Кроме того, в процессе арифметизации [math]Q_1 \ldots Q_m \phi(x_1, \ldots, x_m)[/math] переходит в [math]R_1 \ldots R_m A_\phi(x_1, \ldots, x_m)[/math]. Поэтому далее будем рассматривать только формулы, которые имеют вид, указанный выше.

Лемма (2):

Пусть [math]Q_1 \ldots Q_m \phi(x_1, \ldots, x_m)[/math] — булева формула с кванторами, переходящая в процессе арифметизации в [math]s = R_1 \ldots R_m A_\phi(x_1, \ldots, x_m)[/math]. [math]c_1, \ldots, c_m[/math] — двоичные константы. Обозначим через [math]A_i(x_{i+1}) = R_{i+2} \ldots R_m A_\phi(c_1, \ldots, c_i, x_{i+1}, \ldots, x_m)[/math], где [math]0 \le i \le m - 1[/math]. Тогда: Если [math]R_1 = \sum[/math], то [math]A_0(0) + A_0(1) = s[/math], если [math]R_1 = \prod[/math], то [math]A_0(0) \cdot A_0(1) = s[/math]. [math]\forall i : 1 \le i \le m - 1[/math] если [math]R_{i+1} = \sum[/math], то [math] A_i(0) + A_i(1) = A_{i-1}(c_i)[/math], если [math]R_{i+1} = \prod[/math], то [math]A_i(0) \cdot A_i(1) = A_{i-1}(c_i)[/math].

Доказательство:

[math]\triangleright[/math]

proof

[math]\triangleleft[/math]