Изменения

Перейти к: навигация, поиск

Sharp SAT

777 байт добавлено, 20:56, 15 апреля 2010
Новая страница: «== Определение == <tex>\#SAT = \{ <\varphi, k> | \varphi</tex> имеет <tex>k</tex> удовлетворяющих наборов <tex>\}</tex> == У…»
== Определение ==

<tex>\#SAT = \{ <\varphi, k> | \varphi</tex> имеет <tex>k</tex> удовлетворяющих наборов <tex>\}</tex>

== Утверждение ==
<tex>\#SAT \in IP</tex>

== Доказательство ==
Пусть формула <tex>\varphi</tex> как-то записана. Сделаем следующие замены:
# <tex>x \land y \to x \cdot y</tex>
# <tex> \lnot x \to 1 - x</tex>
# <tex> x \lor y \to x + y - x \cdot y = 1 - (1 - x) \cdot (1 - y)</tex>
Заметим, что длина формулы возрастет не на много.

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

Навигация