Sharp SAT — различия между версиями

Материал из Викиконспекты
Перейти к: навигация, поиск
(Новая страница: «== Определение == <tex>\#SAT = \{ <\varphi, k> | \varphi</tex> имеет <tex>k</tex> удовлетворяющих наборов <tex>\}</tex> == У…»)
 
(нет различий)

Версия 21:42, 17 апреля 2010

Определение

[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].