# Subset Sum to SAT reduction

I have seen numerous ways to reduce CNF-SAT to SS, but is there any way to reduce SS to SAT (or one of its variations)? I have tried researching it, but all it brings up is the (apparently) much more common opposite reduction.

• Are you familiar with Cook's theorem? Jul 29, 2019 at 0:04
• Does this answer your question? Reduce subset sum to 3SAT Nov 4, 2020 at 1:38

You can reduce addition to a circuit with XOR, AND, OR gates.

Each element of the sum must first be ANDed with an extra variable that is true if the element belongs to the subset, and false otherwise.

Then the circuit can be trivially reduced to 3-SAT. The clauses are determined by the gates.

For example each AND gate (A & B = C) requires these 4 clauses:

(A | !B | !C)

(!A | B | !C)

(A | B | !C)

(!A | !B | C)

Why? Because:

false & true != true

true & false != true

false & false != true

true & true != false

Each clause eliminates one impossible situation for the gate.

Then if you want the result of the sum to be zero, you add one unit clause for each bit of the result.