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

Материал из Викиконспекты
Перейти к: навигация, поиск
м (rollbackEdits.php mass rollback)
 
(не показаны 4 промежуточные версии 4 участников)
Строка 1: Строка 1:
 
Введём понятие арифметизации булевых формул. Пусть нам дана формула <tex>\phi(x_1 \ldots x_m)</tex>. Сделаем следующие преобразования и получим формулу <tex>A_\phi(x_1, x_2, \ldots, x_m)</tex>:
 
Введём понятие арифметизации булевых формул. Пусть нам дана формула <tex>\phi(x_1 \ldots x_m)</tex>. Сделаем следующие преобразования и получим формулу <tex>A_\phi(x_1, x_2, \ldots, x_m)</tex>:
 
* <tex>x_i \to x_i</tex>;
 
* <tex>x_i \to x_i</tex>;
* <tex>\lnot x \to 1 - x</tex>;
+
* <tex>\lnot \varphi \to 1 - A_\varphi</tex>;
 
* <tex>\varphi \land \psi \to A_\varphi \cdot A_\psi</tex>;
 
* <tex>\varphi \land \psi \to A_\varphi \cdot A_\psi</tex>;
 
* <tex>\varphi \lor \psi \to 1 - (1 - A_\varphi) \cdot (1 - A_\psi)</tex>;
 
* <tex>\varphi \lor \psi \to 1 - (1 - A_\varphi) \cdot (1 - A_\psi)</tex>;
Строка 10: Строка 10:
 
|about=1
 
|about=1
 
|statement=<tex>\phi(x_1 \ldots x_m) = A_\phi(x_1, \ldots, x_m)</tex>.
 
|statement=<tex>\phi(x_1 \ldots x_m) = A_\phi(x_1, \ldots, x_m)</tex>.
|proof=
+
|proof=Непосредственно следует из построения.
proof
 
 
}}
 
}}
  
Строка 39: Строка 38:
 
Докажем пункты 1.1 и 2.1. Для остальных пунктов доказательство аналогично.
 
Докажем пункты 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>
+
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>
 +
 
 +
Тогда
  
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>
+
<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>.
 
}}
 
}}

Текущая версия на 19:13, 4 сентября 2022

Введём понятие арифметизации булевых формул. Пусть нам дана формула [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 \varphi \to 1 - A_\varphi[/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]
Непосредственно следует из построения.
[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]. Тогда:

    1. Если [math]R_1 = \sum[/math], то [math]A_0(0) + A_0(1) = s[/math];
    2. Если [math]R_1 = \prod[/math], то [math]A_0(0) \cdot A_0(1) = s[/math].
  1. [math]\forall i : 1 \le i \le m - 1[/math]
    1. Если [math]R_{i+1} = \sum[/math], то [math] A_i(0) + A_i(1) = A_{i-1}(c_i)[/math];
    2. Если [math]R_{i+1} = \prod[/math], то [math]A_i(0) \cdot A_i(1) = A_{i-1}(c_i)[/math].
Доказательство:
[math]\triangleright[/math]

Докажем пункты 1.1 и 2.1. Для остальных пунктов доказательство аналогично.

1.1. [math]s=\sum\limits_{x_1 = 0}^{1}R_2\ldots R_m(x_1, x_2, \ldots, x_m)=R_2 \ldots R_m[/math][math](0, x_2, \ldots, x_m) + R_2 \ldots R_m(1, x_2, \ldots, x_m)=A_0(0) + A_0(1)[/math].

2.1. [math]A_{i-1}(c_i)=\sum\limits_{x_{i+1} = 0}^{1}R_{i+2}\ldots R_m[/math][math](c_1, \ldots, c_{i-1}, c_i, x_{i+1}, \ldots x_m)=R_{i+2} \ldots R_m[/math][math](c_1, \ldots, c_i, 0, x_{i+2}, \ldots, x_m) + R_{i+2} \ldots R_m[/math][math](c_1, \ldots, c_i, 1, x_{i+2}, \ldots, x_m)=A_i(0) + A_i(1)[/math].
[math]\triangleleft[/math]
Определение:
Оператором линеаризации будем называть оператор [math]L_{i}A(x_i)=(1-x_i) \cdot A[/math][math](0)+x_i \cdot A(1)[/math].

Заметим, что оператор линеаризации уменьшает степень [math]x_i[/math] до единицы, при этом полученная формула эквивалентна исходной. Кроме того, если дано выражение [math]R_1 \ldots R_m A_\phi(x_1, \ldots, x_m)[/math], то [math]L_{i}[/math] можно вставить в список [math]R_1,\ldots,R_m[/math] в любое место, после операции [math]R_i[/math] (для того, чтобы выражение, на которое действует оператор, было функцией от [math]x_i[/math]). При этом значение выражения не изменится. Операторы [math]L_i[/math] и [math]L_j[/math] можно вставлять в выражение независимо друг от друга для любых [math]1 \le i, j \le m[/math]. Для оператора линеаризации можно сформулировать лемму, аналогичную лемме (2).

Лемма (3):
Пусть [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)=R_1 \ldots R_{i+1} L_j R_{i+2}\ldots R_m A_\phi(x_1, \ldots, x_m)[/math], [math]j \lt i + 2[/math].

[math]c_1, \ldots, c_m[/math] — двоичные константы.

[math]A_{i}'(x_1,\ldots,x_{i+1}) = L_j R_{i+2} \ldots R_m A_\phi(x_1, \ldots, x_m)[/math]

[math]A_{i}(x_1,\ldots,x_{i+1}) = R_{i+2} \ldots R_m A_\phi(x_1, \ldots, x_m)[/math]

Тогда

[math]A_i'(c_1,\ldots,c_{i+1}) = (1-c_j) \cdot A_i[/math][math](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})[/math].