Sharp SAT

Определение

[math]\#SAT = \{ \lt \varphi, k\gt | \varphi[/math] имеет [math]k[/math] удовлетворяющих наборов [math]\}[/math]

Утверждение

[math]\#SAT \in IP[/math]

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

Пусть формула [math]\varphi[/math] как-то записана. Сделаем следующие замены:

1. [math]x \land y \to x \cdot y[/math]
2. [math] \lnot x \to 1 - x[/math]
3. [math] x \lor y \to x + y - x \cdot y = 1 - (1 - x) \cdot (1 - y)[/math]

Заметим, что длина формулы возрастет не на много.

Итак, надо проверить следующее уравнение: [math]\sum_{x_1 = 0}^{1}\sum_{x_2 = 0}^{1}...\sum_{x_n = 0}^{1} A(x_1, x_2, ..., x_n) = k[/math].