There is a following logical optimization problem.
$$\text{Max} \text{ } \text{OF} = z$$ $$\text{S.t:} \quad (x+y=1) \implies (z \leq 20)$$ $$x,y \in \text{{0,1}} ,z \in \mathbb{R}^+$$
I know, there are some linearizations to solve such a problem efficiently. But, What I am getting stuck on is if, one equals the term $(x+y)$ to a new auxiliary variable, in this case $w$, how can ensure it consists of all of the feasible solution space? Let's say if, one turns out the above logical constraint into $x+y \geq 1-w$ and then replaces the original logical constraint to $(w=1) \implies (z \leq 20)$, The problem may solve with an optimal solution, but it seems to allow $(x,y,w)=(1,1,1)$ and disallow $(x,y,w)=(0,0,0)$.
As $x$ and $y$ are binary, the solution space and its combination would be, (if I am thinking wrong please, correct me): there exist four combinations and three possible feasible solutions for $x+y$. $\text{ {(0,0),(0,1),(1,0),(1,1)} }$ combinations respectively, and $\text{ {0,1,2} }$ feasible solution space.
Also, I tried $(x+y \geq 1-w)$, $(x+y=w)$, etc. but, in all of the cases, the optimal solution is the same as the solvers like Gurobi, CPLEX, and Pyomo-GDP returned by whose specific logical modeling features!!!
My main question is, how we can actually ensure that the solution we can achieve by linearization is really feasible when the optimal solution is the same as the reported solution by the solver?
One of the users on the OR site suggested something like this: $ x+y = 2*v+w$ where $ 0 \le v \le 1$ is binary while $ 0 \le w \le 1$. Then the usual
$ z \le 20w + z_{max}(1-w)$.
$ v$ can be binary but I always try with relaxation to see if that works.