RSA (FACT) to SAT transform complexity

Question

Is it possible to transform RSA (FACT) to SAT during polynomial time? (Polynomial number of variables and clauses of logical formula and polynomial time of creating logical formula).

The size of the task is obviously the number of bits $n$.

Answer 1

Absolutely yes (it must be because SAT is NP-complete). The easiest way to do it is analogous to computer hardware. You encode the multiplication of two $n$-bit numbers as a logic-network (of size $O(n^2)$, and that in turn can be translated into a SAT formula (of size $O(n^2)$ again). For the second step you might want to look up "Tseytin transformation".

Though I should mention that in practice this is not useful. Factorizing algotihms like poolard-rho and number-sieve algorithms are A LOT faster then encoding into SAT and using a sat-solver on that problem. Comparative experiments are regularly done by the sat-solving community.