Boolean functions satisfying a condition

Question

What is the total number of Boolean functions $f :\{0,1\}^n \rightarrow \{1,-1\}$ such that

\begin{equation}\tag{1}\label{e} \sum_xf(x)f(x+y) = 0 \end{equation}

for all $0\neq y$?

Is there some closed form construction to obtain them all? Or even one specific example if it exists at all? I tried to use inverse Fourier transform but no luck.

For $n = 2$ one such example is $f(00) = f(10) = f(01) = 1$ and $f(11) = -1$. But for larger $n$ it seems very difficult.

Note that $f$ cannot be additive.

EDIT: Alex below claims that no such functions exist for $n >2$. However, for $n =4$, I was able to construct (very ad-hoc) the following

Columns 1 through 14

 0     0     0     0     0     0     0     0     1     1     1     1     1     1
 0     0     0     0     1     1     1     1     0     0     0     0     1     1
 0     0     1     1     0     0     1     1     0     0     1     1     0     0
 0     1     0     1     0     1     0     1     0     1     0     1     0     1
 1    -1     1     1     1     1    -1     1     1     1     1    -1     1    -1

Columns 15 through 16

One way to to think of this is by considering the function $f_y: x \mapsto f(x)f(x+y)$ and impose that $f_y$ is additive for all $y$. So the question now becomes:

Question: Does there exist $\hat{y}$ such that $f_y = \chi_{\hat{y}}: x\mapsto (-1)^{\hat{y}x^T}$.

Then \eqref{e} becomes a simple consequence of characters.

Your $n=4$ example does not look right. For $y ,in {2, 6, 10}$ the sum is not $0$. — Axel Kemper, Nov 14 '20 at 12:34
Well, I manually checked $y = 2 = 0010$ and the sum is zero. o not sure what's going on. — user 1987, Nov 14 '20 at 13:36
Might be a misunderstanding on my side. Could you run (or look at) the check code, I added to my answer? — Axel Kemper, Nov 14 '20 at 13:43
The discrepancy between @AxelKemper and original poster's view is in the meaning of the "plus" sign in $f(x+y)$. It seems Axel's answer is treating it as usual addition of numbers modulo $2^n$, while the question is treating the arguments as binary vectors of length $n$ so their addition is component-wise modulo $2$ (i.e. 0001+0001 = 0000 rather than 0010). — Peter Košinár, Nov 17 '20 at 21:52

Axel Kemper · Answer 1 · 2020-11-14T13:01:18.373

I have tried to find solutions using the Python interface of Microsoft's Z3 solver.

My Z3PY model:

from z3 import *
n = 2
noOfMinterms = 2 << (n-1)
print("n = %s" % n)
print("minterm rows = %s" % noOfMinterms)
Minterms = [i for i in range(noOfMinterms)]
define truth table with one Bool variable for every row
table = []
for i in Minterms:
    table += [Bool("b" + str(i))]
def f(x):
    return If(table[x % noOfMinterms], 1, -1)
s = Solver()
for y in range(1, noOfMinterms):
    s.add(Sum([Product(f(x), f(x + y)) for x in Minterms]) == 0)
solutions = 0
while s.check() == sat:
    m = s.model()
    solutions += 1
    print(str(solutions) + ": ", [" 1 " if is_true(m[table[i]]) else "-1 " for i in Minterms])
    #  prevent the solution to be found again
    s.add(Or([table[i] != m[table[i]] for i in Minterms]))
if solutions == 0 :
    print("No solutions found. Sorry")
else:
    print("Solutions: %s" % solutions)

Output for $n = 2$:

n = 2
minterm rows = 4
1:  [' 1 ', '-1 ', ' 1 ', ' 1 ']
2:  ['-1 ', ' 1 ', ' 1 ', ' 1 ']
3:  [' 1 ', '-1 ', '-1 ', '-1 ']
4:  [' 1 ', ' 1 ', ' 1 ', '-1 ']
5:  [' 1 ', ' 1 ', '-1 ', ' 1 ']
6:  ['-1 ', ' 1 ', '-1 ', '-1 ']
7:  ['-1 ', '-1 ', ' 1 ', '-1 ']
8:  ['-1 ', '-1 ', '-1 ', ' 1 ']
Solutions: 8

The solution mentioned in the question is number $4$ of the $8$ solutions.

For $n$ larger than $2$, no solution was found.

MiniZinc also does not find solutions for $n \gt 2$:

include "globals.mzn";
int: n = 2;
int: noOfMinterms = pow(2, n);
set of int: Minterms = 0 .. noOfMinterms - 1;
array[Minterms] of var bool: X; %  true = 1; false = -1
constraint

forall(y in Minterms where y != 0) (
   sum([f(x) * f(x+y) | x in Minterms]) == 0
);
function var int: f(int: x) = if X[x mod noOfMinterms] then 1 else -1 endif;
function int: f2(Minterms: x) = if fix(X[x]) then 1 else -1 endif;
solve satisfy;
output ["(n): "] ++
       [show_int(3, f2(i)) | i in Minterms];

Check code in C# for given solutions:

int n = 4;
int noOfMinterms = (2 << (n - 1));
int[] f = { 1, -1, 1, 1, 1, 1, -1, 1, 1, 1, 1, -1, 1, -1, -1, -1 };
for (int y = 1; y < noOfMinterms; y++)
{
    int sum = 0;
for (int x = 0; x &lt; noOfMinterms; x++)
{
   sum += f[x] * f[(x + y) % noOfMinterms];
}

Console.WriteLine($&quot;{y} {sum}&quot;);

}

score 0 · Answer 2 · answered Nov 17 '20 at 22:56

Following Peter Košinár's comment, I modified my Z3 model to use bit-wise exclusive or for $x+y$ rather than addition modulo $2$:

from z3 import *
n = 4
noOfMinterms = 2 << (n-1)
print("n = %s" % n)
print("minterm rows = %s" % noOfMinterms)
Minterms = [i for i in range(noOfMinterms)]
define truth table with one Bool variable for every row
table = []
for i in Minterms:
    table += [Bool("b" + str(i))]
def f(x):
    return If(table[x], 1, -1)
s = Solver()
for y in range(1, noOfMinterms):
    s.add(Sum([Product(f(x), f(x ^ y)) for x in Minterms]) == 0)
solutions = 0
while s.check() == sat:
    m = s.model()
    solutions += 1
    print(str(solutions) + ": ", [" 1 " if is_true(m[table[i]]) else "-1 " for i in Minterms])
    #  prevent the solution to be found again
    s.add(Or([table[i] != m[table[i]] for i in Minterms]))
if solutions == 0 :
    print("No solutions found. Sorry")
else:
    print("Solutions: %s" % solutions)

The numbers of solutions for small $n$:

n   # Solutions
2      8
3      0
4      896
5      ?

The modified MiniZinc model:

include "globals.mzn";
int: n = 4;
set of int: Bits = 0 .. n;
%  pre-calculate powers of 2: 1, 2, 4, ...
array[Bits] of int: twopow = array1d(Bits, [pow(2, i) | i in Bits]);
int: noOfMinterms = twopow[n];
set of int: Minterms = 0 .. noOfMinterms - 1;
array[Minterms] of var bool: X; %  true = 1; false = -1
constraint

forall(y in Minterms where y != 0) (
   sum([f(x) * f(bitxor(x, y)) | x in Minterms]) == 0
);
%  function to calculate the biwise xor of two ints
%  cf. https://en.wikipedia.org/wiki/Bitwise_operation#XOR
function int: bitxor(Minterms: x, Minterms: y) =
  sum([twopow[i] * (((x div twopow[i]) + (y div twopow[i])) mod 2) | i in Bits]);
function var int: f(int: x) = if X[x] then 1 else -1 endif;
function int: f2(Minterms: x) = if fix(X[x]) then 1 else -1 endif;
solve satisfy;
output ["(n): "] ++
       [show_int(3, f2(i)) | i in Minterms];

The modified check code in C# which confirms the example solution from the question:

int n = 4;
int noOfMinterms = (2 << (n - 1));
int[] f = { 1, -1, 1, 1, 1, 1, -1, 1, 1, 1, 1, -1, 1, -1, -1, -1 };
for (int y = 1; y < noOfMinterms; y++)
{
    int sum = 0;
for (int x = 0; x &lt; noOfMinterms; x++)
{
    sum += f[x] * f[(x ^ y) % noOfMinterms];
}

Console.WriteLine($&quot;{y} {sum}&quot;);

}

Boolean functions satisfying a condition

2 Answers2

define truth table with one Bool variable for every row

define truth table with one Bool variable for every row