Предполагается, что Y(x1,…, xi,…,xm) представлено формулой
полиномиальной сложности.
Вот здесь мне видятся основные проблемы.
Насчет бесповторных функций - для бесповторных функций существует полиномиальный алгоритм распознавания выполнимости. Набросок алгоритма:
Алгоритм принимает на вход бесповторную формулу и выдает

, если она тождественно ложна,

- если тождественно истинна, и

в остальных случаях.
1. Находим главный символ формулы (линейно отн. длины формулы)
2. Запускаем алг. рекурсивно для двух подформул, связанных главным символом.
3. определяем результат для формулы (например,

,

,

,

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

). В частности, некоторые таким образом построенные алгоритмы рассматриваются в книге В. Б. Алексеева "Введение в теорию сложности алгоритмов".