Let's say, in order to linearize the product of the two binary variables the logical condition would be, z <=> (x and y), where x, y, and z are binary. The corresponding CNF form is as follows:
\begin{align*} & z \iff x \wedge y \\ & \left(z \implies (x \wedge y)\right) \bigwedge \left((x \wedge y) \implies z\right) \\ & \left(\neg z \vee (x \wedge y)\right) \bigwedge \left(\neg(x \wedge y) \vee z\right) \\ & \left((\neg z \vee x) \wedge (\neg z \vee y)\right) \bigwedge \left((\neg x \vee \neg y) \vee z\right) \\ & (\neg z \vee x) \bigwedge (\neg z \vee y) \bigwedge (\neg x \vee \neg y \vee z) \\ & \left((1 - z) + x \ge 1\right) \bigwedge \left((1 - z) + y \ge 1\right) \bigwedge \left((1 - x) + (1 - y) + z \ge 1\right) \\ & (x \ge z) \bigwedge (y \ge z) \bigwedge (z \ge x + y - 1) \end{align*}
and the last line is exactly what can be translated in the math form as three linear inequalities. Now, my question is about the last line in the following expressions that I can translate from logic to math from original expression as $\sum_{i=1}^{n} x_{i} = 2 \implies \delta = 1$, where $x_i$ and $\delta$ are binary:
$$ \text{exactly(2)}_i x_i \implies \delta = 1 $$ $$ \text{atleast(2)}_i x_i \land \text{atmost(2)}_i x_i \implies \delta = 1$$ $$ \lnot (\text{atleast(2)}_i x_i \land \text{atmost(2)}_i x_i) \lor \delta$$ $$ (\text{atmost(2-1)}_i x_i \lor \text{atleast(2+1)}_i x_i) \lor \delta$$ $$ (\text{atmost(1)}_i x_i \lor \text{atleast(3)}_i x_i) \lor \delta$$ $$ (\sum_{i=1}^n x_{i} \leq 1) \lor ((\sum_{i=1}^n x_{i} \geq 3) \lor \delta$$
Now, as it seems, the last line obviously needs the auxiliary binary variables to form a CNF in order to make indicators constraints. Would you please, is there any way to go deeper into the above logical form to making a CNF that can be directly converted to the math inequalities? (something like the last line of CNF form of product of the two binary variables is)?
Here's an approach that avoids introducing any additional variables, and the conjunctive normal form somewhat automatically yields $\binom{n}{2}$ linear constraints: $$ \left(\bigvee_{i<j} \left(x_i \land x_j\land \bigwedge_{k \notin \{i,j\}} \lnot x_k\right)\right) \implies \delta \\ \lnot \left(\bigvee_{i<j} \left(x_i \land x_j\land \bigwedge_{k \notin \{i,j\}} \lnot x_k\right)\right) \lor \delta \\ \left(\bigwedge_{i<j} \lnot \left(x_i \land x_j\land \bigwedge_{k \notin \{i,j\}} \lnot x_k\right)\right) \lor \delta \\ \left(\bigwedge_{i<j} \left(\lnot x_i \lor \lnot x_j \lor \bigvee_{k \notin \{i,j\}} x_k\right)\right) \lor \delta \\ \bigwedge_{i<j} \left(\lnot x_i \lor \lnot x_j \lor \bigvee_{k \notin \{i,j\}} x_k \lor \delta\right) \\ (1 - x_i) + (1 - x_j) + \sum_{k \notin \{i,j\}} x_k + \delta \ge 1 \quad \text{for all $i<j$} \\ x_i + x_j - \sum_{k \notin \{i,j\}} x_k - 1 \le \delta \quad \text{for all $i<j$} \\ $$ Indeed, if $x_i=1$ and $x_j=1$ and all other $x_k=0$, then the LHS is $1$, which forces $1 \le \delta$ (hence $\delta=1$), as desired.