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

If you want a shorter formula, I suggest using logic synthesis, e.g., Quine-McClusky, Espresso.

The usual path to get a small formula is to allow introduction of additional variables, build a circuit (e.g., an adder circuit followed by a comparator), then convert to a formula using the Tseitin transform. This yields much smaller formulas, but it requires introducing extra variables, which you said you don't want.

| cite | improve this answer | |

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.