I have a big LP program with around $91,000$ variables and $2,900,000$ constraints. They are all binary variables, but I want to try also relaxing the problem putting $0 \le x \le 1$ bounds. I am not very knowledgeable on the subject because I took only one university course on operations research about 30 years ago and didn't use it afterwards, so I forgot nearly everything.
The problem is aimed at trying to prove the union closed sets conjecture for a given fixed number of sets. I have formulated it implementing this answer and this answer.
The formulation is:
$$\max \sum_{i=1}^n a_{1,i} \tag1\label1$$
subject to:
$$\sum_{i=1}^n a_{k,i} \ge \lfloor n/2 \rfloor + 1, \space 2 \le k \le q \tag2\label2$$ $$a_{k,\ell} \le a_{k,i} + 1 - z_{i,j,\ell}, \space 1 \le k \le q, 1 \le i \lt j \le n, 1 \le \ell \le n \tag3\label3$$ $$a_{k,\ell} \le a_{k,j} + 1 - z_{i,j, \ell}, \space 1 \le k \le q, 1 \le i \lt j \le n, 1 \le \ell \le n \tag4\label4$$ $$a_{k,\ell} \ge a_{k,i} + a_{k,j} + z_{i,j,\ell} - 2, \space 1 \le k \le q, 1 \le i \lt j \le n, 1 \le \ell \le n \tag5\label5$$ $$\sum_{\ell=1}^n z_{i,j,\ell} = 1, \space 1 \le i \lt j \le n \tag6\label6$$ $$x_{k,i,j} \le a_{k,i} + a_{k,j} \le 2-x_{k,i,j}, \space 1 \le k \le q, 1 \le i \lt j \le n \tag7\label7$$ $$\sum_{k=1}^q x_{k,i,j} \ge 1, \space 1 \le k \le q, 1 \le i \lt j \le n \tag8\label8$$
with all binary values. Some of the $\eqref{3}$, $\eqref{4}$, $\eqref{5}$, can be eliminated or simplified when $\ell = i$ or $\ell = j$. There are many alternatives for $\eqref{1}$ and $\eqref{2}$, for example we can order the occurrences of elements from element $1$ to $q$ and then again search the maximum occurrence of element $1$.
This is actually the dual formulation of the union closed sets conjecture, because we are considering intersection-closed families of sets (the intersection of any two sets must still belong to the family), and if the conjecture is true there must exist at least one element in at most $\lfloor n/2 \rfloor$ sets.
The matrix with elements $a_{i,j}$ represent the family of sets: a column is one set, while a row represents an element (well, there can be two or more identical rows, in which case we can think they represent a single element). There are $n$ columns (the given fixed number of sets) and $q$ rows (the maximum number of elements).
Therefore $\eqref{1}$ checks the occurrences of an element (element 1) that we expect to be at most $\lfloor n/2 \rfloor$. Constraint $\eqref{2}$ forces all the other elements to be in more than $\lfloor n/2 \rfloor$ sets. $\eqref{3}$, $\eqref{4}$, $\eqref{5}$ and $\eqref{6}$ require that the family be intersection closed (the intersection of any two sets [columns] must still belong to the family [matrix]) and finally $\eqref{7}$ and $\eqref{8}$ forces all sets to be different. Note that we can also use these last two constraints, needed by the problem, that enforce all sets to be different, for the purpose of replacing $=$ with $\ge$ in $\eqref{6}$.
I have written a smaller version of the program ($n=11$, $q=4$) with LP file format and submitted it successfully to the NEOS server. At the moment I am producing the LP files through a specific C program for my problem.
However, the "big" case, with $n=53$ and $q=13$, has an LP file of size $130$ MByte. NEOS server accepts a maximum of $16$ MByte.
The conjecture has been proven for $n \lt 53$, so $n = 53$ is the lowest number of sets for which a proof is missing, as of today. Note that there is a theorem that limits the maximum number of elements of a counterexample to $13$ for $n = 53$ (the minimal counterexample must have $n \ge 4q+1$, where $n$ is the number of sets and $q$ the number of elements).
Any suggestion for a file format which is both concise in size and quick to learn? Also, are $91,000$ variables and $2,900,000$ constraints too much for the NEOS server?
I have run cases $n=23, q=6$ and $n=29, q=7$ at NEOS with Gurobi, but it timed out after 8 hours.
Any other suggestion for attempting the $n=53$ and $q=13$ case?
