# How to transform this logical if-then constraint?

Consider the binary variables $$x, y, z \in \{0,1\}$$.

I'd like to formulate the two if-then constraints:

$$x + y \geq 2 \implies z = 0, \tag{1}$$ $$x + y \leq 1 \implies z = 1. \tag{2}$$

Constraint (1) can be formulated as

$$x + y \leq 2 - z.$$

How to proceed for (2) ?

Indeed, for the first constraint you can use: $$x+y+z \le 2$$
For the second one, it might be easier to model the contraposition: $$z=0 \quad \Rightarrow \quad x+y \ge 2 \quad \Rightarrow \quad x=y=1$$
This yields: $$1-z \le x \\ 1-z \le y$$
You want to linearize $$xy=1-z$$. See https://or.stackexchange.com/a/473/500 for a somewhat automatic derivation of a linearization for $$xy=z$$ via conjunctive normal form. You can then replace $$z$$ with $$1-z$$ in the resulting constraints.