Maximize the minimal distance between true variables in a list

Question

I'm using the OR-Tools CP-SAT solver on a list of $n$ boolean variables $x_i$. I'm trying to maximize the minimal distance between two true variables in this list, as illustrated by the following figure.

+---+---+---+---+---+---+---+---+---+---+---+---+---+---+---+---+---+---+
| 0 | 0 | 1 | 0 | 0 | 0 | 1 | 0 | 0 | 1 | 0 | 0 | 0 | 0 | 1 | 0 | 0 | 0 |
+---+---+---+---+---+---+---+---+---+---+---+---+---+---+---+---+---+---+
           <-------------> <---------> <----------------->
                  4             3               5
                            (minimum)

In other words, mathematically, I'm trying to maximize the expression : $$\min(j-i \mid 0 < i < j < n, x_i = x_j = 1)$$

At the moment, I'm using this algorithm, basically brute-forcing all the possible intervals:

minimalDistance = model.NewIntVar(0, n);
for (k = 1; k < n; ++k) {
    isIntervalAtLeastOfGivenSize[k] = model.NewBoolVar();
    model.AddEquivalence(
        isIntervalAtLeastOfGivenSize[k],
        minimalDistance >= k
    );
}
for (i = 0; i < n; ++i) {
    for (j = i + 1; j < n; ++j) {
        model.AddImplication(
            x[i] and isIntervalAtLeastOfGivenSize[j - i + 1],
            x[j] = false
        )
    }
}
model.maximize(minimalDistance)
model.solve()

It works, but I have a feeling that it's not the best approach: it adds a lot of constraints, and it doesn't scale well when $n$ gets bigger. Is there a better way to do it?

Answer 1

You can maximize $z$ subject to linear big-M constraints $$z - (j-i) \le M_{ij} (2 - x_i - x_j),$$ where $M_{ij} = n-(j-i)$. Each such constraint enforces the logical implication $(x_i \land x_j) \implies z \le j - i$.

If you also know a lower bound $\sum_i x_i \ge k$ for some $k > 1$, you can impose a valid constraint $$z \le \left\lfloor\frac{n-1}{k-1}\right\rfloor$$ that dominates some of the other constraints.

Answer 2

I have no idea (i) whether the following can be encoded in a CP solver and (ii) how efficient it would be. On the pro side, it only requires a linear number of variables and constraints.

Say you have $n$ boolean variables $x_{0}, ..., x_{n-1}$. You can introduce an integer-valued counter $s_{0}, ..., s_{n-1}$ such that $$ s_{0} = \left\{ \begin{array}{ll} n & \text{ if } x_{0} = 0\\ 0 & \text{ if } x_{0} = 1 \end{array} \right. \qquad s_{i} = \left\{ \begin{array}{ll} n & \text{ if } x_{i} = 0 \land s_{i-1}=n\\ s_{i-1} + 1 & \text{ if } x_{i} = 0\land s_{i-1} \neq n\\ 0 & \text{ if } x_{i} = 1 \end{array} \right. $$ This counter starts from $n$, is incremented as long as $x$ remains zero and if it's not equal to $n$, and is reset to $0$ every time $x$ takes value one.

From there, we can just maximize $z$, subject to the additional constraints :

$$x_i = 1 \Rightarrow z \leq s_{i-i}$$

For the example you gave in the original question, this would yield something like

  +---+---+---+---+---+---+---+---+---+---+---+---+---+---+---+---+---+---+
x | 0 | 0 | 1 | 0 | 0 | 0 | 1 | 0 | 0 | 1 | 0 | 0 | 0 | 0 | 1 | 0 | 0 | 0 |
  +---+---+---+---+---+---+---+---+---+---+---+---+---+---+---+---+---+---+
s | n | n | 0 | 1 | 2 | 3 | 0 | 1 | 2 | 0 | 1 | 2 | 3 | 4 | 0 | 1 | 2 | 3 |
  +---+---+---+---+---+---+---+---+---+---+---+---+---+---+---+---+---+---+
            ↑               ↑           ↑                   ↑
          z ≤ n           z ≤ 3       z ≤ 2               z ≤ 4
        (trivial)                   (stronger)

Answer 3

Probably I'm not understanding correctly the problem, but to me the solution looks like

(n - X) / (X - 1)

with X being the number of 1 (True values) in the array of lenght n

Suppose you have an array of 9 variables. 3 True, 6 False: the above formula gives you:

(9 - 3) / (3 - 1) = 3

In fact you can arrange your 9 variable this way:

1 | 0 | 0 | 0 | 1 | 0 | 0 | 0 | 1