0
$\begingroup$

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.

$\endgroup$
1

1 Answer 1

2
$\begingroup$

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

  1. 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.
  2. You could implement an addition tree with additional variables and clauses.
  3. 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.

$\endgroup$

Your Answer

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

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