0
$\begingroup$

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?

$\endgroup$
4
  • 1
    $\begingroup$ cs.stackexchange.com/q/13188/755, cs.stackexchange.com/q/6521/755, cs.stackexchange.com/q/38007/755 $\endgroup$
    – D.W.
    Commented May 15, 2022 at 0:29
  • $\begingroup$ @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. $\endgroup$
    – TLW
    Commented May 15, 2022 at 4:02
  • $\begingroup$ 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. $\endgroup$
    – D.W.
    Commented May 15, 2022 at 7:20
  • 1
    $\begingroup$ 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. $\endgroup$
    – Kyle Jones
    Commented May 15, 2022 at 21:23

0

Your Answer

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

Browse other questions tagged or ask your own question.