Fast Reduction from RSA to SAT
One approach to encode Factoring (RSA) to SAT is to use multiplicator circuits (every circuit can be encoded as CNF).
Let's assume we are given an integer $C$ with $2n$ bits, $C=(c_1,c_2,\cdots,c_{2n})_2$. We are interested in finding two $n$-bit integers $A=(a_1,\cdots,a_n)$ and $B=(b_1,\cdots,b_n)$ whose product is $C=A*B$.
The most naive encoding can be something like this; we know that:
$$c_{2n}= a_n \land b_n$$
$$c_{2n-1}= (a_n\land b_{n-1}) xor (a_{n-1}\land b_n)$$
$$Carry:d_{2n-1}= (a_n\land b_{n-1}) \land (a_{n-1}\land b_n)$$
$$c_{2n-2}= (a_n\land b_{n-2}) xor (a_{n-1}\land b_{n-1}) xor (a_{n-2}\land b_{n}) xor d_{2n-1}$$
...
Then using Tseitin transformation, the above encoding can be translated into CNF.
This approach produces a relatively small CNF. But this encoding does not support &quot;Unit Propagation&quot; and so, the performance of SAT Solvers are really bad.
There are other circuit for multiplication which can be used for this purpose, but they produce a larger CNF.