Sufficient condition for linear separability of a boolean function on $n$ variables

Question

This is a cross-post of two recent questions at math.stackexchange without answers: Q1 and Q2.

A boolean function on an $n$-dimensional hypercube is linearly separable when the convex hulls of the points evaluating to $0$ and $1$ respectively are disjoint.

A necessary condition is that any rectangle (not only the faces) formed by $4$ points of the hypercube is linearly separable.

Is this condition also sufficient?

I have tested that the number of linearly separable boolean functions (OEIS A000609) on $n \le 4$ variables is equal to the number of hypercubes with all rectangles formed by $4$ vertices linearly separable (these ones counted using this answer and this software). Therefore the above condition is proven sufficient for $n \le 4$.

Using the suggestion on the below comment by @Fedor Petrov I was able to prove the conjecture for $n \le 5$ using this updated software which took about $8$ minutes on my computer, which decreases to about $5$ minutes if I test the next boolean function on the rectangle where the previous one failed the linear separability test.

UPDATE 2024-02-13

Using this software I was able to compute the expected value of $15028134$ for $n=6$ in $22$ hours, so now the conjecture is proven for $n \le 6$. Later this other software did it even better in $2$ hours and $45$ minutes. However now it looks impossible to go further searching for a possible counterexample, unless a more advanced algorithm, exploiting some structure of the problem and with much lower computational complexity, is found.

UPDATE 2024-02-16

A new software, exploiting some symmetry, computed the case $n = 6$ in only $2$ seconds and the expected value $8378070864$ for $n = 7$ in $1$ hour and $19$ minutes. Therefore now the conjecture is true for $n \le 7$.

Answer 1

The condition is not sufficient. This is a counterexample for $n=9$:

3121716732950836191359193754534242007469797427570571637452595771886175474823117400353574287579547318923874761239430570584653046830442366504009727

It satisfies the rectangle condition, but is not linearly separable.

I found it by noticing that sets $a$

(1,1,1,0,0,0,0,0,0)
(0,0,0,1,1,1,0,0,0)
(0,0,0,0,0,0,1,1,1)

and $b$

(1,0,0,1,0,0,1,0,0)
(0,1,0,0,1,0,0,1,0)
(0,0,1,0,0,1,0,0,1)

were linearly inseparable, and also had the property that no rectangle with opposite corners in $a$ had any corners in $b$, and vice versa.

Here's some SageMath code to verify

x = 3121716732950836191359193754534242007469797427570571637452595771886175474823117400353574287579547318923874761239430570584653046830442366504009727

p = MixedIntegerLinearProgram(maximization=True, solver='PPL')
v = p.new_variable(real=True)
for i in range(512):
    s = sum(v[j]*((i>>j)&1) for j in range(9)) + v['c']
    if x&(1<<i):
        p.add_constraint(s >= 0)
        p.add_constraint(v['o'] <= s)
    else:
        p.add_constraint(s <= 0)
        p.add_constraint(v['o'] <= -s)
p.add_constraint(v['o'] <= 1)
p.set_objective(v['o'])
print(p.solve(), p.get_values(v)) # objective value of 0 means not separable

import itertools

def gen_rectangles(n):
    x = []
    for t in itertools.product([
        (0,0,0),
        (1,1,1),
        (0,0,1),
        (1,1,0),
        (0,1,0),
        (1,0,1),
    ], repeat=n):
        a = b = c = 0
        for a1, b1, c1 in t:
            a, b, c = a*2+a1, b*2+b1, c*2+c1
        if a < b < c:
            x.append((a, b, c, a^^b^^c))
    return x

for a,b,c,d in gen_rectangles(9):
    t = ((x>>a)&1, (x>>b)&1, (x>>c)&1, (x>>d)&1)
    if t in [(0,1,1,0), (1,0,0,1)]:
        print('Found bad rectangle:', a, b, c, d)
        break

```