Modeling equality in an ILP

Lets say we have integer variables $$a \in\mathbb{Z}^n$$ and $$M \in\{0,1\}^{n\times L}$$. I am promised $$a_i \leq L$$, for some fixed constant $$L$$. I want to model the constraint $$M_{i,j} \iff (a_i=j)$$ in an integer linear program. What is the most efficient way to do this in an ILP? In particular, can I do this without Big-M constraints and without breaking down each integer into its binary representation?

Currently I can see two ways to model this:

Option 1

We can apply the method described in the answer here to the constraint $$M_{i,j} \iff (a_i-j=0)$$. This requires $$1$$ extra binary variable as well as $$4$$ potentially large "Big M" constraints per $$M_{i,j}$$, thus resulting in $$nL$$ new binary variables and $$4nL$$ new big M constraints.

Option 2

We can break down $$a_i$$ into its bits using $$\log L$$ extra binary variables. We can also compute the corresponding binary bit breakdowns for each $$0\leq j \leq L$$. Let $$bit^{(a)}_{i,k}$$ be the $$k$$th bit of $$a_i$$ and let $$bit_{j,k}^*$$ be the $$k$$th bit of the integer $$j$$, so that $$a_i = \sum_{k=0}^{\log L}2^kbit^{(a)}_{i,k}.$$

We now have the following logic: $$M_{i,j} \iff (\forall k . 0\leq k\leq \log L \implies bit^{(a)}_{i,k} \odot bit_{j,k}^*)$$

Therefore

$$M_{i,j} = \bigwedge_{k=0}^{\log L} bit^{(a)}_{i,k} \odot bit_{j,k}^*.$$

We can use this post to NXOR the pairs of variables, storing their results as another variable $$z=\{0,1\}^{\log L}$$. We can AND these together using the constraints $$M_{i,j} \ge \sum z_i$$ $$M_{i,j} \leq z_i \;\;\; \forall i$$

This creates $$\log L$$ new variables and 1 constraint for representing the binary breakdown of $$a_i$$. We then have $$\log L$$ XNOR variables, each which can be represented with 4 constraints. We can finally represent $$M_{i,j}$$ with $$\log L + 1$$ more constraints. Therefore, we have a total of $$5\log L$$ constraints and $$2\log L$$ new variables per $$M_{i,j}$$, giving us a total of $$5nL\log L$$ new binary constraints and $$2nL\log L$$ new binary variables.

Is there some third option that is better than either of these two options?

• It looks to me like your count of variables and constraints for option 2 is off; shouldn't it be $2 \log L$ variables and $5 \log L$ constraints per entry of $M$, i.e., a total of $2nL\log L$ variables and $5nL \log L$ constraints? – D.W. Apr 27 at 17:55
• Yes, it is the same for option 1, (both are per entry). Would you recommend changing it? – Bryce Kille Apr 27 at 18:06
• Yeah, since you say "total", I think so. – D.W. Apr 27 at 18:13

I have several options for you. Here is the simplest:

1.1 Direct Option

Use an inequality to enforce that one out of $$M_{i,1},\dots,M_{i,L}$$ are true:

$$M_{i,1} + \dots + M_{i,L} = 1.$$

Use a second inequality to link that to $$a_i$$:

$$a_i = M_{i,1} + 2 M_{i,2} + 3 M_{i,3} + \dots + L M_{i,L}.$$

2 Indirect Options

Alternatively, we could try to follow more closely to the approach you outlined, but using ideas from one-out-of-n constraints for SAT solvers. In particular, the entries $$M_{i,1},\dots,M_{i,L}$$ are a one-hot encoding of a one-out-of-L constraint, and you want them to be consistent with an encoding directly as an integer. There are standard techniques for enforcing one-out-of-n constraints for SAT, and you could using them with ILP as well.

2.1 Improved Binary Encoding

We can use the idea in https://cs.stackexchange.com/a/51512/755 to improve your option 2. Let $$a_{i,k}$$ denote the $$k$$th bit of $$a$$. We add the constraint

$$M_{i,j} \implies a_{i,k} \text{ if } bit^*_{j,k}=1,$$

otherwise add the constraint

$$M_{i,j} \implies \neg a_{i,k} \text{ if } bit^*_{j,k}=0.$$

Next, we add the constraint

$$M_{i,1} + \dots + M_{i,L} \ge 1.$$

This requires only $$n+nL\log L$$ constraints and $$n\log L$$ new variables, instead of $$5nL \log L$$ constraints and $$2nL \log L$$ new variables.

Commander Encoding

You could use a a recursive commander encoding to enforce that exactly one out of $$M_{i,1},\dots,M_{i,L}$$ are true. Note that the constraint for "at most one variable in a group can be true" requires $$O(m^2)$$ clauses in SAT but can be represented in a single inequality in ILP, so the number of constraints needed will be smaller than for SAT. Then, you could use any of the above techniques to link the $$M$$'s to the $$a'$$.

That said, I don't expect these indirect options to be worth implementation; my expectation is that the direct option will be more natural, and it is what I would try first.