Linearize product of $x\cdot y \text{ with } x,y \in \{-1,0,1\}$ for MILP

Question

I have a problem where I have many products between variables drawn out of $\{-1,0,1\}$. Could you suggest a linearization in terms of variables in $\{-1,0,1\}$ or $B_1 - B_2$ where $B_i \in \{0,1\}$ possibly with a constraint like $1\geq B_1 + B_2$ or $1 \leq B_1 + B_2$ to get rid of double encoding of $0$ when found helpful.

I tried to find a way to construct this using the linearization of the product of Booleans but I found no way to do so elegantly (that is do so without implementing the CNF of the Karnaugh diagram for $B_1$, $B_2$ of the result). The fact that such a CNF encoding is possible suggests that there might exist a more appropriate formulation for MILP.

Answer 1

If you write $x=B_1-B_2$, $y=B_3-B_4$, and $z=B_5-B_6$ and supply the nine solutions for which $z=x\cdot y$, $B_1+B_2 \le 1$, $B_3+B_4 \le 1$, and $B_5+B_6 \le 1$, PORTA returns $B_i \ge 0$ and the following seven inequalities: \begin{align} - B_1 - B_3 + B_6 &\le 0 \\ - B_1 - B_4 + B_5 &\le 0 \\ - B_2 - B_3 + B_5 &\le 0 \\ - B_2 - B_4 + B_6 &\le 0 \\ - B_1 - B_2 + B_5 + B_6 &\le 0 \\ - B_3 - B_4 + B_5 + B_6 &\le 0 \\ B_1 + B_2 + B_3 + B_4 - B_5 - B_6 &\le 1 \end{align} The resulting system has only the nine originating solutions.