Convert RSA-1024 to propositional formula

Question

Context

I am struggling with converting FACT to SAT, RSA-1024 is my ultimate goal. My strategy is to convert a long multiplication circuit to a propositional formula. I have been trying to understand how the carry-save adder is working but I don't know how to calculate the carry-on.

What I got so far

In the multiplication circuit, I will be dealing with big numbers and will have to sum more than 3 numbers, since it's binary it means that carry-on will split into several digits, let's say $K$ digits, after summing-up $N$ numbers. So here is what I found:

• $k_1 = (a_1 \lor a_2... \lor a_{N-1}) \land (a_2 \lor a_3... \lor a_{N}) \land (a_1 \lor a_3... \lor a_{N})$ Ex: for $N = 3$: $(a_1 \lor a_2) \land (a_2 \lor a_3) \land (a_3 \lor a_1)$
• $k_2$ = same as with $k_1$ but instead of having $N-1$ length clauses, have $N-3$ length clauses with all the possible selections.
• For the general case have $N-2^K + 1$ length clauses with all the possible selections.

Question

It's easy to see how my solution creates an exponential number of clauses, can you please suggest me a better approach?

Answer 1

Short version: Sounds like you have written down your adding circuit with a gate in it that has O(N) inputs. This tends to lead to exponential numbers of clauses like you are experiencing. The solution is to break up gates with lots of inputs into gates with just 2 inputs before converting to clauses.

Long version: It's best to do it in stages. First break each addition operation into a series of add-with-carry elements, then break each of those into its basic component logic gates (AND, OR, XOR, NOT). Note that the fundamental gates all have either 1 input (NOT) or two inputs (AND, OR, XOR). If you want to compute the XOR of 4 inputs, you can chain 3 2-input XOR gates together, similarly if you want to compute the AND or OR of lots of inputs.

Finally, it is possible to make any of the basic gates using O(1) clauses: You simply add an extra variable for the output of the gate and refer to that variable whenever you want to use the output. Some clauses must be added to enforce the input/output relation that defines the gate, but since the gate has just 1 output and at most 2 inputs, the number of clauses required is O(1), and a fairly low O(1) at that.