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.
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)
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.