Encoding SAT EqualsK Constraint with Two Possible Values

Question

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.

Answer 1

One option is to use a normal EqualsK, as

$$(t \lor \text{Equals}(A,x_1 \cdots x_n)) \land (\neg t \lor \text{Equals}(B,x_1 \cdots x_n))$$

where $t$ is a fresh variable. It is easy to convert this to CNF by distributing the $t \lor \cdots$ into the clauses of the EqualsK constraints.

(Why does this work? If $\varphi,\psi$ are two boolean formulas and $t$ is a fresh new variable, then $(t \lor \varphi) \land (\neg t \lor \psi)$ is equisatisfiable with $\varphi \lor \psi$: e.g., if $\varphi$ is satisfiable, you can set $t$ to False, or if $\psi$ is satisfiable, you can set $t$ to True.)

Another option is to count the number of true values, using a boolean adder circuit, and build another small circuit to compare the output of the adder to $A$ and to $B$, and then convert this circuit to CNF using the Tseitin transform. If $A < B \le n$, this can be done using $O(n \lg B)$ clauses and new variables.

If you are working with a solver in practice, if it supports pseudo-boolean constraints, you can use those to express your condition.

Related: Encoding 1-out-of-n constraint for SAT solvers, Reduce the following problem to SAT.