# Convert (x + y = z) to propositional logic formula for 8-bit numbers

(Note: this was asked in the cstheory stackexchange, but I was told this is a more appropriate place for it.)

I have three 8-bit 2's-complement numbers (X, Y, and Z). I want to find a propositional logic formula using only the variables (x1, x2... x8, y1... y8, z1... z8), where xi is the ith bit of x which expresses the concept that X + Y = Z. How would I go about doing this?

You can obtain a formula in CNF form by writing down a truth table (with $2^{24}$ rows) and then converting each row to a single clause. This will yield a formula with $2^{24}$ clauses, but the method is straightforward.