Let me first introduce the problem. I have prepared an illustrative picture.
There is a blue box with $I$ inputs. Blue box contains $Y$ yellow boxes. Each yellow box contains $R$ red boxes. Each red box has up to $X$ inputs. One needs to connect blue box inputs with red boxes inputs. Single blue box input can be connected to multiple red boxes. Red box input can be connected only with single blue box input or can be left unconnected. How the inputs are connected is constrained by the requirements (well, first one needs to answer the question if meeting all requirements is even possible). All requirements have the same structure, each one can be characterized by 3 numbers.
Single requirement is a tuple $(\gamma, \sigma, \mu)$. It should be understood as follows. There is at least $\gamma$ yellow boxes, with at least $\sigma$ red boxes, with at least $\mu$ inputs connected to distinct blue box inputs. In other words, $\gamma \times \sigma \times \mu$ distinct blue box inputs must be connected to $\gamma \times \sigma$ red boxes within $\gamma$ yellow boxes. For given requirement, the number of required red boxes within yellow boxes is equal, so is the number of red boxes inputs. For example, if $\mu = 2$ one can not connect 1 input in one red box and 3 inputs in some other red box. All requirements meet the following conditions: $\gamma \le Y$, $\sigma \le R$, $\mu \le X$.
In my case $I=42$, $Y=6$, $R=8$, $X=5$. I wanted to approach this problem as a SAT problem. As each blue box input can be connected to any given red box input, it implies that there must be $I \times Y \times R \times X = 42 \times 6 \times 8 \times 5 = 10080$ boolean variables. The number of variables is not large as for boolean SAT problem.
However, the number of clauses I get is enormous. This means that:
- I'm stupid and I am encoding clauses in a wrong way.
- Approaching the problem as a SAT problem is a bad idea.
- Both 1 and 2.
How do I encode the requirements? Well, I generate all possible scenarios for given requirement as I haven't got a better idea. For example, one of the requirements is as follows $(1, 8, 5)$. This means, that there must be at least 1 yellow box, with 8 red boxes with 5 inputs connected to 40 distinct blue box inputs. Generating all possible scenarios for this particular requirement is sick, as for single yellow box the variation equals $\frac{42!}{(42-40)!}$.
I would really appreciate if someone gives me advice if treating this problem as a SAT problem is good idea or explains me how to generate clauses for this problem efficiently.