1
$\begingroup$

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.

$\endgroup$

1 Answer 1

0
$\begingroup$

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.

$\endgroup$
2
  • $\begingroup$ Thanks for the answer! I am indeed using a solver right now to solve some problem, and the first option works. Can you explain intuitively why it works? $\endgroup$ May 9 at 8:46
  • $\begingroup$ @TimBersama, Cool, I'm glad it was useful! Thank you for letting me know. I have edited my answer to explain why it works. $\endgroup$
    – D.W.
    May 9 at 9:22

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.