Вычисление количества единичных значений булевой функции

[0101]

Есть NP полная задача определения выполнимости булевых фунций (БФ). В отличие от общего случая, для конкретных классов булевых функций есть «простые» решения.
Одна из очевидных стратегий получения такого решения.
Для любой БФ можно получить формулу в каноническом виде, которая позволяет вычислить количество единичных значений, с учетом того что часть аргументов задана, а часть принимает все возможные значения. (Мат. аппарат давно известен и применяется, в частности, для расчета надежности электрических схем –т.н. Логико – вероятностное исчисление). Очевидно, что эта формула позволяет решать уравнение, построенное на заданной БФ. Сложность получения решения будет прямопропорциональна сложности формулы. Т. е. практическая польза канонической формы представления формулы невелика. Нужно искать компактную форму.
Конкретный пример.
Есть циклическое S произведение 2-х четырехразрядных двоичных чисел X и Y.
S=2^3 s4+2^2 s3 +2^1 s2 + 2^0 s1
X=2^3 x4+2^2 x3 +2^1 x2 + 2^0 x1
Y=2^3 y4+2^2 y3 +2^1 y2 + 2^0 y1
Для s4 - s1 существуют понятные компактные формулы.
Путем очевидных и не очень действий получаю s1- s4 в алгебраическом виде.
Полагая соотв. аргументы равными 0,1/2, 1 можем вичислять количество единичных значений (КЕЗ)
КЕЗ s1= 256 s1=256(x1 y1 + x4 y2 - 2 x1 x4 y1 y2 + x1 x3 x4 y1 y2 + x3 y3 - 2 x1 x3 y1 y3 + x2 x4 y1 y3 - x1 x2 x4 y1 y3 - x2 x3 x4 y1 y3 + 2 x1 x2 x3 x4 y1 y3 - 2 x3 x4 y2 y3 + x2 x3 x4 y2 y3 + x1 x2 x3 y1 y2 y3 - x2 x4 y1 y2 y3 + 2 x1 x2 x4 y1 y2 y3 + x3 x4 y1 y2 y3 + 2 x1 x3 x4 y1 y2 y3 - 4 x1 x2 x3 x4 y1 y2 y3 + x2 y4 - 2 x1 x2 y1 y4 + x1 x2 x4 y1 y4 + x1 x3 y2 y4 - x1 x2 x3 y2 y4 - 2 x2 x4 y2 y4 - x1 x3 x4 y2 y4 + 2 x1 x2 x3 x4 y2 y4 - x1 x3 y1 y2 y4 + 2 x1 x2 x3 y1 y2 y4 + x1 x4 y1 y2 y4 + 2 x1 x2 x4 y1 y2 y4 + x2 x3 x4 y1 y2 y4 - 4 x1 x2 x3 x4 y1 y2 y4 - 2 x2 x3 y3 y4 + x1 x2 x3 y3 y4 + x1 x2 y1 y3 y4 + 2 x1 x2 x3 y1 y3 y4 - x2 x4 y1 y3 y4 + x1 x3 x4 y1 y3 y4 + 2 x2 x3 x4 y1 y3 y4 - 4 x1 x2 x3 x4 y1 y3 y4 - x1 x3 y2 y3 y4 + x2 x3 y2 y3 y4 + x1 x2 x4 y2 y3 y4 + 2 x1 x3 x4 y2 y3 y4 + 2 x2 x3 x4 y2 y3 y4 - 4 x1 x2 x3 x4 y2 y3 y4 + 2 x1 x3 y1 y2 y3 y4 - 4 x1 x2 x3 y1 y2 y3 y4 + 2 x2 x4 y1 y2 y3 y4 - 4 x1 x2 x4 y1 y2 y3 y4 - 4 x1 x3 x4 y1 y2 y3 y4 - 4 x2 x3 x4 y1 y2 y3 y4 + 11 x1 x2 x3 x4 y1 y2 y3 y4).
Можно выполнить замены чтобы поставлять -1,0,1.
Но из каких соображений искать компатную форму? Ничего очевидного в голову не пришло и в литературе не нашлось…