Определение свойств программы (функции) по коду (формуле)

[Xaositect]

Ales в сообщении #320875 писал(а):

А разве тогда из факта отсутствия подсказки нельзя вывести, что решения нет?
Или это будет не по правилам?

А вот здесь и вылезает экспоненциальный перебор. В принципе, если перебирать все возможные наборы в качестве подсказок, то мы либо найдем решение, либо докажем, что его нет.

-- Вт май 18, 2010 00:08:17 --

В общем, NP и coNP - это "зеркально" похожие классы - для NP есть подсказка, позволяющая доказать истинность свойства, а для coNP - ложность.

[Ales]

Xaositect в сообщении #320873 писал(а):

Ну можно придумать достаточно простые свойства, которые, скорее всего, ни в NP, ни в coNP не лежат.
Вот например, дана функция от переменных.

Этот вопрос фактически про функцию со значениями в $\mathbb B^{2^k}$.
Может быть в "разумном" свойстве нельзя разделять переменные, на y и z?

-- Вт май 18, 2010 00:19:15 --

Xaositect в сообщении #320877 писал(а):

А вот здесь и вылезает экспоненциальный перебор. В принципе, если перебирать все возможные наборы в качестве подсказок, то мы либо найдем решение, либо докажем, что его нет.

Не понятно. Нам сказали "подсказки нет и не будет".
Значит решения нет (ведь если бы оно существовало, нам бы его сообщили бы и была бы подсказка), или не так?

[Xaositect]

Ales в сообщении #320881 писал(а):

Может быть в "разумном" свойстве нельзя разделять переменные, на y и z?

Ох, ну я могу и еще что-нибудь придумать.
Вот, скажем, есть функция $f\colon\mathbb{B}^k\to\mathbb{B}$, верно ли, что существует $x$ такое, что в $x$ не более $k/2$ единиц и $f(y) = 1$ для любого $y$, полученного из $x$ заменой каких-то нулей на единицы?

-- Вт май 18, 2010 00:30:34 --

Ales в сообщении #320881 писал(а):

Не понятно. Нам сказали "подсказки нет и не будет".

Ну, в определении NP сказано, что если подсказку дали, то можно проверить. А про то, когда ее нет, ничего не сказано.

Грубо говоря, мы не верим тому, кто дает подсказку. Если ее дали, то мы быстро проверяем, что все действительно правильно. А если нам сказали "такого набора нет", то мы быстро это проверить не сможем.

[Ales]

Xaositect в сообщении #320885 писал(а):

Ох, ну я могу и еще что-нибудь придумать.
Вот, скажем, есть функция , верно ли, что существует такое, что в не более единиц и для любого , полученного из заменой каких-то нулей на единицы?

Наверное лучше пойти в обратную сторону. Понять как могут выглядеть свойства, которые так можно формализовать.
Таким образом, проскочим первый этап и можно перейти ко второму: сравнения проверки свойства и проверки тавтологии.

-- Вт май 18, 2010 00:33:35 --

Xaositect в сообщении #320885 писал(а):

Грубо говоря, мы не верим тому, кто дает подсказку. Если ее дали, то мы быстро проверяем

А если он дал неверную подсказку?

-- Вт май 18, 2010 00:35:50 --

Тут какая то теория.
А в жизни похоже все одно и то же.
Если найдем быстрый алгоритм для одного, то и другое проверим.

[Xaositect]

Ales в сообщении #320889 писал(а):

Наверное лучше пойти в обратную сторону. Понять как могут выглядеть свойства, которые так можно формализовать.
Таким образом, проскочим первый этап и можно перейти ко второму: сравнения проверки свойства и проверки тавтологии.

Ну это есть почти определение coNP - если свойство выразимо в виде $p(x_1,\dots,x_n,f(x_1),\dots,f(x_n)) = 1$, $p$ - полиномиально вычислимо, $n = k^{O(1)}$, то оно принадлежит классу coNP.
Тавтология - это самая сильная coNP-задача, т.е. coNP-полная: если мы умеем определять тавтологию, то можем и любую coNP-задачу решить. Обратное неверно, но, скорее всего, некоторый класс функций $p$, при котором задачи таки будут coNP-полными, очертить можно.

-- Вт май 18, 2010 00:39:33 --

Ales в сообщении #320889 писал(а):

Тут какая то теория.
А в жизни похоже все одно и то же.
Если найдем быстрый алгоритм для одного, то и другое проверим.

Если найдем - то да.

Ales в сообщении #320889 писал(а):

А если он дал неверную подсказку?

То мы попытаемся ее проверить, и у нас не получится. Мы скажем, что подсказка неверная, а вопрос о том, существует ли решение, останется открытым.

[Ales]

Xaositect в сообщении #320885 писал(а):

Ох, ну я могу и еще что-нибудь придумать.

Наверное, свойства вида $f(g(x))\equiv 1$ тоже так не формализуются.