<p>This is a hard problem, but there are a number of approaches.</p>
<ol>
<li>You could encode the constraint directly in CNF. This would require <span class="math-container">$\binom{n}{k}$</span> clauses. In your case, this is around <span class="math-container">$10^{27}$</span> so not practical.</li>
<li>You could implement an addition tree with additional variables and clauses.</li>
<li>You could use a pseudo-boolean solver and encode the constraint directly.</li>
</ol>
<p>I'll focus on the second approach since there's not much to say on the others.</p>
<p>You'll need adders and half-adders. An adder takes three inputs and returns a high bit and a low bit; a half adder takes only two inputs and returns a high bit and a low bit.</p>
<p>An adder takes 13 clauses:</p>
<pre><code>p cnf 4 7
c x4 = PARITY(x1, x2, x3)
c c4 is the low bit of an adder.
1 2 3 4 0
1 2 -3 4 0
1 -2 -3 4 0
-1 2 -3 4
-2 3 -4 0
-1 3 -4 0
-1 -2 -4 0

p cnf 4 6
c x4 = MAJORITY(x1, x2, x3)
c c4 is the high bit of an adder.
1 2 4 0
1 3 4 0
2 3 4 0
-2 -3 -4 0
-1 -3 -4 0
-1 -2 -4 0
</code></pre>
<p>A half-adder takes 7 clauses:</p>
<pre><code>p cnf 3 4
c x3 = x1 XOR x2 = PARITY(x1, x2)
c c3 is the low bit of a half-adder.
1 2 -3 0
1 -2 3 0
-1 2 3 0
-1 -2 -3 0


p cnf 3 3
c x3 = x1 AND x2
c c3 is the high bit of a half-adder.
-1 -2 3 0
1 -3 0
2 -3 0
</code></pre>
<p>A half-adder can reduce <span class="math-container">$n$</span> bits into <span class="math-container">$\lfloor n/3\rfloor$</span> high bits and <span class="math-container">$\lfloor n/3\rfloor + n-3\lfloor n/3\rfloor$</span> low bits. Recursing it takes at most <span class="math-container">$(n-1)/2$</span> adders and 1 half-adder (perhaps there is some better combination) for a total of <span class="math-container">$(13n+1)/2$</span> clauses to reduce <span class="math-container">$n$</span> bits to 1 low bit and <span class="math-container">$&lt; n/2$</span> high bits, or <span class="math-container">$\approx 13n$</span> clauses and <span class="math-container">$\approx n$</span> new variables to reduce the bits to a binary representation. (You'll also need <span class="math-container">$\log_2(n)$</span> clauses for the hamming equality itself.)</p>
<p>These can be reduced somewhat if you know that the very highest bits are forced to be 0 (or, indeed, if you can prove the value of any fixed bit). You may also be able to do better still if you have constraints on certain subsets of the bits. For example, if you are able to group the bits such that, in any 3, at most one is 1, you can reduce the three to one bit with an OR:</p>
<pre><code>p cnf 4 4
c x4 = OR(x1, x2, x3)
1 2 3 -4 0
-3 4 0
-2 4 0
-1 4 0
</code></pre>
<p>This alone would reduce the clauses from <span class="math-container">$13n$</span> to <span class="math-container">$14n/3$</span> and the variables from <span class="math-container">$n$</span> to <span class="math-container">$2n/3.$</span> Obviously this depends a lot on the shape of your problem! In the best case, where you can group them into 10s (since you have 200/20 = 10 variables per expected 1) you could reduce much further. At this point you should look into <a href="https://en.wikipedia.org/wiki/Quine%E2%80%93McCluskey_algorithm" rel="nofollow noreferrer">Quine-McCluskey</a> and minimize an expression with &quot;Don't Care&quot; for all combinations with more than the allowed number of bits set.</p>

CC BY-SA 4.0
2022-12-27T20:35:31.827Z
2022-12-27T20:35:31.827Z
Charles
<p>I have a SAT problem in conjunctive normal form that I’d like to solve, but I need to add one more condition: for the existing variables <span class="math-container">$x_1,\ldots,x_n$</span> the Hamming weight is <span class="math-container">$k$</span>. (It would be ok to require the weight to be <span class="math-container">$\ge k$</span>, but in fact any solutions will have exactly <span class="math-container">$k$</span>.)</p>
<p>What is an efficient way to add this condition to my CNF formula? There’s a good literature on efficient circuits for Hamming weight but I don’t know how well those would survive translation.</p>
<p>For reference, the cases I’m currently considering have <span class="math-container">$n\approx200$</span> and <span class="math-container">$k\approx20$</span> but I’d like to go much further using a SAT solver (maybe minisat).</p>
<p>I’m happy to add additional variables if that’s the best way to do it.</p>

CC BY-SA 4.0
2022-12-27T06:08:41.020Z
https://cs.stackexchange.com/q/6521/755, https://cs.stackexchange.com/q/13188/755, https://stackoverflow.com/q/43081929/781723
D.W.
<cc.complexity-theory><sat>
Require Hamming weight in CNF
Charles
# Require Hamming weight in CNF

(Asked by: username_0 on 2022-12-26)

I have a SAT problem in conjunctive normal form that I’d like to solve, but I need to add one more condition: for the existing variables $x\_1,\ldots,x\_n$ the Hamming weight is $k$. (It would be ok to require the weight to be $\ge k$, but in fact any solutions will have exactly $k$.)

What is an efficient way to add this condition to my CNF formula? There’s a good literature on efficient circuits for Hamming weight but I don’t know how well those would survive translation.

For reference, the cases I’m currently considering have $n\approx200$ and $k\approx20$ but I’d like to go much further using a SAT solver (maybe minisat).

I’m happy to add additional variables if that’s the best way to do it.

**Tags:** cc.complexity-theory, sat

> **Comments:**
> **username_1**: https://cs.stackexchange.com/q/6521/755, https://cs.stackexchange.com/q/13188/755, https://stackoverflow.com/q/43081929/781723  

---

## 1 answers

### Answer by username_0 on 2022-12-27. Score: 2

This is a hard problem, but there are a number of approaches.

You could encode the constraint directly in CNF. This would require $\binom{n}{k}$ clauses. In your case, this is around $10^{27}$ so not practical.
You could implement an addition tree with additional variables and clauses.
You could use a pseudo-boolean solver and encode the constraint directly.

I'll focus on the second approach since there's not much to say on the others.
You'll need adders and half-adders. An adder takes three inputs and returns a high bit and a low bit; a half adder takes only two inputs and returns a high bit and a low bit.
An adder takes 13 clauses:
p cnf 4 7
c x4 = PARITY(x1, x2, x3)
c c4 is the low bit of an adder.
1 2 3 4 0
1 2 -3 4 0
1 -2 -3 4 0
-1 2 -3 4
-2 3 -4 0
-1 3 -4 0
-1 -2 -4 0

p cnf 4 6
c x4 = MAJORITY(x1, x2, x3)
c c4 is the high bit of an adder.
1 2 4 0
1 3 4 0
2 3 4 0
-2 -3 -4 0
-1 -3 -4 0
-1 -2 -4 0

A half-adder takes 7 clauses:
p cnf 3 4
c x3 = x1 XOR x2 = PARITY(x1, x2)
c c3 is the low bit of a half-adder.
1 2 -3 0
1 -2 3 0
-1 2 3 0
-1 -2 -3 0


p cnf 3 3
c x3 = x1 AND x2
c c3 is the high bit of a half-adder.
-1 -2 3 0
1 -3 0
2 -3 0

A half-adder can reduce $n$ bits into $\lfloor n/3\rfloor$ high bits and $\lfloor n/3\rfloor + n-3\lfloor n/3\rfloor$ low bits. Recursing it takes at most $(n-1)/2$ adders and 1 half-adder (perhaps there is some better combination) for a total of $(13n+1)/2$ clauses to reduce $n$ bits to 1 low bit and $< n/2$ high bits, or $\approx 13n$ clauses and $\approx n$ new variables to reduce the bits to a binary representation. (You'll also need $\log_2(n)$ clauses for the hamming equality itself.)
These can be reduced somewhat if you know that the very highest bits are forced to be 0 (or, indeed, if you can prove the value of any fixed bit). You may also be able to do better still if you have constraints on certain subsets of the bits. For example, if you are able to group the bits such that, in any 3, at most one is 1, you can reduce the three to one bit with an OR:
p cnf 4 4
c x4 = OR(x1, x2, x3)
1 2 3 -4 0
-3 4 0
-2 4 0
-1 4 0

This alone would reduce the clauses from $13n$ to $14n/3$ and the variables from $n$ to $2n/3.$ Obviously this depends a lot on the shape of your problem! In the best case, where you can group them into 10s (since you have 200/20 = 10 variables per expected 1) you could reduce much further. At this point you should look into Quine-McCluskey and minimize an expression with "Don't Care" for all combinations with more than the allowed number of bits set.


---

