I am wondering about a way to CNF encode an EqualsK constraint with two possible values. In other words, I want to solve for the equation:
$$ (\sum_{i=1}^n x_i = A) \lor (\sum_{i=1}^n x_i = B) $$
There are CNF encodings already discussed for encoding EqualsK constraints with one value K, like here for instance, where the property $\text{Equals}(k, (x_1, \dots, x_n)) \equiv \text{AtLeast}(k, (x_1, \dots, x_n)) \land \text{AtMost}(k, (x_1, \dots, x_n))$ is used.
I have considered using just the normal EqualsK and adding an OR operation in the middle, but this results in it no longer being in CNF. Any help is very much appreciated, even a slow or naive encoding is fine. Thanks in advance.