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}^*)$$


$$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?

  • $\begingroup$ 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? $\endgroup$
    – D.W.
    Apr 27 '19 at 17:55
  • $\begingroup$ Yes, it is the same for option 1, (both are per entry). Would you recommend changing it? $\endgroup$ Apr 27 '19 at 18:06
  • 1
    $\begingroup$ Yeah, since you say "total", I think so. $\endgroup$
    – D.W.
    Apr 27 '19 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.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.