Implications and Equivalences Between Booleans

In constraint programming, we often need to express logical relationships between boolean variables. The most basic is the implication $b_1 \to b_2,$ read as "if $b_1$ then $b_2$."

The truth table is

$$\begin{array}{|c|c|c|} \hline b_1 & b_2 & b_1 \to b_2 \\ \hline 0 & 0 & 1 \\ 0 & 1 & 1 \\ 1 & 0 & 0 \\ 1 & 1 & 1 \\ \hline \end{array}$$

The implication is false only when $b_1 = 1$ and $b_2 = 0;$ a false hypothesis makes the implication vacuously true.

To encode $b_1 \to b_2$ in OR-Tools' CP-SAT, we use $\texttt{OnlyEnforceIf}{:}$

$$\texttt{model.Add(b2 == 1).OnlyEnforceIf(b1)}$$

This activates the constraint $b_2 = 1$ exactly when $b_1$ is true. When $b_1 = 0,$ the constraint is dormant, so $b_2$ may take either value -- matching the truth table.