Meaning of infeasible model: unsuccessful solving for an IP model with binary variables

Question

For fun, I have modeled the Union-closed sets conjecture for a universe of a given size into a problem with binary variables.

Each binary variable $x_k$ is the indicator of the set with elements being the positions of the digit $1$ in the binary representation of $k$. For example $x_{13}$ is $1$ if the set $\{0,2,3\}$ belongs to the family. Variables for sets with size less than $3$ are removed because the conjecture is already proven with those sets in the family. Also, if we have $n$ elements, $x_{2^n-1}$ can be replaced with a fixed $1$ because that is the universe. I have added constraints to guarantee that the family is union-closed and that it does not have an element in at least half of the sets. The latter is impossible if the conjecture holds, therefore I expect no solution to the IP problem.

For example, with $n=5$ elements, the model is this:

max: x7+x11+x13+x14+x15+x19+x21+x22+x23+x25+x26+x27+x28+x29+x30;
x7+x11-x15<=1;
x7+x13-x15<=1;
x7+x14-x15<=1;
x7+x19-x23<=1;
x7+x21-x23<=1;
x7+x22-x23<=1;
x11+x13-x15<=1;
x11+x14-x15<=1;
x11+x19-x27<=1;
x11+x25-x27<=1;
x11+x26-x27<=1;
x13+x14-x15<=1;
x13+x21-x29<=1;
x13+x25-x29<=1;
x13+x28-x29<=1;
x14+x22-x30<=1;
x14+x26-x30<=1;
x14+x28-x30<=1;
x19+x21-x23<=1;
x19+x22-x23<=1;
x19+x25-x27<=1;
x19+x26-x27<=1;
x21+x22-x23<=1;
x21+x25-x29<=1;
x21+x28-x29<=1;
x22+x26-x30<=1;
x22+x28-x30<=1;
x25+x26-x27<=1;
x25+x28-x29<=1;
x26+x28-x30<=1;
x7+x11+x13-x14+x15+x19+x21-x22+x23+x25-x26+x27-x28+x29-x30<=-2;
x7+x11-x13+x14+x15+x19-x21+x22+x23-x25+x26+x27-x28-x29+x30<=-2;
x7-x11+x13+x14+x15-x19+x21+x22+x23-x25-x26-x27+x28+x29+x30<=-2;
x7+x11+x13+x14+x15-x19-x21-x22-x23+x25+x26+x27+x28+x29+x30<=-2;
x7-x11-x13-x14-x15+x19+x21+x22+x23+x25+x26+x27+x28+x29+x30<=-2;
bin x7,x11,x13,x14,x15,x19,x21,x22,x23,x25,x26,x27,x28,x29,x30;

I have solved the problem with LPSolve and got:

Model name:  'LPSolver' - run #1
Objective:   Maximize(R0)

SUBMITTED
Model size:       35 constraints,      15 variables,          165 non-zeros.
Sets:                                   0 GUB,                  0 SOS.

Using DUAL simplex for phase 1 and PRIMAL simplex for phase 2.
The primal and dual simplex pricing strategy set to 'Devex'.

The model is INFEASIBLE
lp_solve unsuccessful after 10 iter and a last best value of -1e+030

MEMO: lp_solve version 5.5.2.11 for 32 bit OS, with 64 bit REAL variables.
In the total iteration count 10, 9 (90.0%) were bound flips.
There were 0 refactorizations, 0 triggered by time and 0 by density.
... on average 1.0 major pivots per refactorization.
The largest [LUSOL v2.2.1.0] fact(B) had 36 NZ entries, 1.0x largest basis.
The maximum B&B level was 1, 0.0x MIP order, with 0 nodes explored.
The constraint matrix inf-norm is 1, with a dynamic range of 1.
Time to load data was 0.002 seconds, presolve used 0.009 seconds,
... 0.012 seconds in simplex solver, in total 0.023 seconds.

The software states explicitly "The model is INFEASIBLE", as I expected, because there can't be any solution.

QUESTION 1: I suppose this can be considered a rigorous proof from a mathematical point of view: am I right?

The same result ("The model is INFEASIBLE") is obtained for $n \le 6$. But for $n = 7$ (and $n=8$) I get:

Model name:  'LPSolver' - run #1
Objective:   Maximize(R0)

SUBMITTED
Model size:     3122 constraints,      98 variables,        10031 non-zeros.
Sets:                                   0 GUB,                  0 SOS.

Using DUAL simplex for phase 1 and PRIMAL simplex for phase 2.
The primal and dual simplex pricing strategy set to 'Devex'.

Relaxed solution                  20 after        549 iter is B&B base.

lp_solve unsuccessful after 1661 iter and a last best value of -1e+030
lp_solve explored 6 nodes before termination

MEMO: lp_solve version 5.5.2.11 for 32 bit OS, with 64 bit REAL variables.
In the total iteration count 1661, 318 (19.1%) were bound flips.
There were 18 refactorizations, 0 triggered by time and 11 by density.
... on average 74.6 major pivots per refactorization.
The largest [LUSOL v2.2.1.0] fact(B) had 10967 NZ entries, 1.0x largest basis.
The maximum B&B level was 4, 0.0x MIP order, with 6 nodes explored.
The constraint matrix inf-norm is 1, with a dynamic range of 1.
Time to load data was 0.005 seconds, presolve used 0.008 seconds,
... 0.609 seconds in simplex solver, in total 0.622 seconds.

so in this case it just says "lp_solve unsuccessful".

QUESTION 2: Can this be considered a proof that there isn't any solution? Or the algorithm just "gave up"?

Edit 2022-04-20

For those who might be interested, I have found some serious research somewhat related to the this post.

Answer 1

It might be worth trying this alternative formulation, with your same $x_k$ variables (one for each of the $2^n$ subsets) and nonnegative slack variables $s_i$. The problem is to minimize $\sum_{i=0}^{n-1} s_i$ subject to \begin{align} x_k + x_\ell - 1 &\le x_{k \cup \ell} &&\text{for $k < \ell$} \tag1 \\ \sum_{k: i \not\in k} x_k - \sum_{k: i \in k} x_k + s_i &\ge 1 \tag2 &&\text{for $i\in \{0,\dots,n-1\}$} \\ \sum_{k \not= 0} x_k &\ge 1 \tag3 \end{align}

Constraint $(1)$ enforces the union-closed property. Constraint $(2)$ prevents element $i$ from appearing in at least half the sets if $s_i=0$. Constraint $(3)$ avoids the trivial family that contains only the empty set. (Note that I include all $2^n$ subsets and do not fix any $x_k$ variables to $0$ or $1$.)

If the LP relaxation has positive optimal objective value, the resulting optimal dual solution provides a short certificate that the conjecture is true.