Why do we need to include formulas of the following form?

$(c_{11}v_1 \wedge \neg c_{11}v_2 \wedge \neg c_{11}v_3 \wedge \neg c_{11}v_4) \lor (\neg c_{11}v_1 \wedge c_{11}v_2 \wedge \neg c_{11}v_3 \wedge \neg c_{11}v_4)\dots$

To ensure that the same number appears only once in every box.

Because otherwise several numbers can be assigned to the same cell

To ensure that the same number appears only once in every row/column.

It is strictly needed only in Sudokus in which the pre-filled cells allow for more than one unique solution.