Subset Sum to SAT 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 &amp; B = C) requires these 4 clauses: 

(A | !B | !C)

(!A | B | !C) 

(A | B | !C) 

(!A | !B | C) 

Why? Because:

false &amp; true != true

true &amp; false != true 

false  &amp; false != true

true &amp; 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.