Converting if-then-else condition to integer linear programming with equality constraints
We have three binary variables $x, y, z \in \{0,1\}$ and the following if-then-else (ITE) condition

$$\text{if } x = 1 \text{ then } y = 1 \text{ else } y = z$$

If $x = 1$, then $y = 1$ but $z \in \{0,1\}$. If $x = 0$, then $y = z \in \{0,1\}$. Therefore, we have the following $4$ vertices of the $3$-cube

$$\{ (0,0,0), (0,1,1), (1,1,0), (1,1,1) \}$$

Using SymPy, we obtain the following product of sums (POS):

&gt;&gt;&gt; from sympy import *
&gt;&gt;&gt; x, y, z = symbols('x y z')
&gt;&gt;&gt; minterms = [[0, 0, 0], [0, 1, 1], [1, 1, 0], [1, 1, 1]]
&gt;&gt;&gt; POSform([x, y, z], minterms, [])
And(Or(Not(x), y), Or(Not(y), x, z), Or(Not(z), y))


Converting the formula in POS, i.e., in conjunctive normal form (CNF), to integer programming, we obtain the following system of linear inequalities

$$\begin{array}{rl} (1-x) + y &amp;\geq 1\\ x + (1-y) + z &amp;\geq 1\\ y + (1-z) &amp;\geq 1\end{array}$$

which can be rewritten as follows

$$\begin{array}{rl} -x + y &amp;\geq 0\\ x - y + z &amp;\geq 0\\ y -z &amp;\geq 0\end{array}$$

Verifying in Haskell:

λ&gt; triples = [ (x,y,z) | x &lt;- [0,1], y &lt;- [0,1], z &lt;- [0,1] ]
λ&gt; filter (\(x,y,z)-&gt;(-x+y&gt;=0) &amp;&amp; (x-y+z&gt;=0) &amp;&amp; (y-z&gt;=0)) triples
[(0,0,0),(0,1,1),(1,1,0),(1,1,1)]