Channeling Between Integer and Boolean Variables

How to link an integer variable to one or more Boolean indicator variables in CP-SAT using OnlyEnforceIf, covering equality indicators, threshold indicators, one-hot encodings, and counting via channeled Booleans.

Step 1 of 157%

Tutorial

Introduction to Channeling

A channeling constraint links an integer variable to one or more Boolean variables so that the Boolean reflects some property of the integer. The most basic case is the equality indicator: we want a Boolean $b$ to be true exactly when an integer variable $x$ equals a fixed value $v$ .

In CP-SAT, the biconditional $b \Leftrightarrow (x = v)$ is enforced as two implications:

b \Rightarrow (x = v) \qquad \text{and} \qquad \neg b \Rightarrow (x \neq v).

We post each implication with OnlyEnforceIf:

model.Add(x == v).OnlyEnforceIf(b)
model.Add(x != v).OnlyEnforceIf(b.Not())

The first line says: when $b$ is true, then $x = v$ . The second says: when $b$ is false, then $x \neq v$ . Together they make $b$ track the truth value of $x = v$ in every solution. Posting only one of the two lines leaves the other direction unconstrained and is a frequent modeling bug.