# Effecient encoding of sum equality in cnf+xor

I am wondering as to how to efficiently encode the following subcircuit for a binary satisfiability solver (cnf, and optionally xor clauses, if this helps):

    eq2 = sum(a, b, c, d, e, f, g, h) == 2
eq3 = sum(a, b, c, d, e, f, g, h) == 3


(All variables binary. That is, eq2 should be set if and only if exactly two of the eight input variables are set; eq3 should be set if and only if exactly 3 of the eight input variables are set.)

This subcircuit appears many times in the problem, so efficient encoding is important.

Things I have tried thus far:

1. Just naively emit the $$2^8$$ miniterms for each. This is simple, but results in 512 clauses of 9 variables each. It also doesn't expose the structure of the problem to the sat solver.
2. Generate the circuits ge2 = or(and(a, b), and(a, c), ...) / ge3 = or(and(a, b, c), and(a, b, d), ...) / ge4 = or(and(a, b, c, d), and(a, b, c, e), ...) / eq2 = and(ge2, ~ge3) / eq3 = and(ge3, ~ge4). This, unfortunately, results in many clauses still.
3. Generate circuits implementing an adder-tree, and then eq2 = and(~sum_3, ~sum_2, sum_1, ~sum_0) and eq3 = and(~sum_3, ~sum_2, sum_1, sum_0). This works, however it unnecessarily constrains the solver (there's a lot of propagation that needs to be done even if the sum is >= 4, for instance), and prevents direct propagation between inputs (they may need to go all the way up the adder-tree and back).

Is there a better method of doing this that I'm missing?

• – D.W.
Commented May 15, 2022 at 0:29
• @D.W. - thank you for the related questions. That being said, this is about setting the output if and only if you have k out of n, not directly requiring exactly k out of n. (And I don't see an easy way to translate from the latter to the former.) Assuming I am understanding the related questions correctly, at least.
– TLW
Commented May 15, 2022 at 4:02
• I suggest reading and thinking about them further. For instance, it's trivial to convert the method based on a sorting network in cs.stackexchange.com/a/51512/755 to set the output as you desire. I suggest spending some time to consider whether you can do the same with the other techniques listed on those questions.
– D.W.
Commented May 15, 2022 at 7:20
• I'll add Reduction of K-Vertex-Cover to SAT: How to define the constraint? to the list of relevant answers since you're keen on solver efficiency. Commented May 15, 2022 at 21:23