Fast Reduction from RSA to SAT

Scott Aaronson's blog post today gave a list of interesting open problems/tasks in complexity. One in particular caught my attention:

Build a public library of 3SAT instances, with as few variables and clauses as possible, that would have noteworthy consequences if solved. (For example, instances encoding the RSA factoring challenges.) Investigate the performance of the best current SAT-solvers on this library.

This triggered my question: What's the standard technique for reducing RSA/factoring problems to SAT, and how fast is it? Is there such a standard reduction?

Just to be clear, by "fast" I don't mean polynomial time. I'm wondering whether we have tighter upper bounds on the reduction's complexity. For example, is there a known cubic reduction?

-

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 $A=(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 "Unit Propagation" 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.

-
In section 6.1 of "Finding Hard Instances of the Satisfiability problem: A survey", by Cook and Mitchell, they use this problem as a challenge. –  Amir May 27 '11 at 6:29
How do you know that A and B must be n bits length, couldn't it be n - 1 and and n bits. For sure it can be 2n bits and 1 bit. –  Ilya_Gazman Oct 17 '13 at 13:14
@Babibu: If we are talking about general factorization, you are right. But for case of RSA, we know that each of the two primes has $n$ bits. –  Amir Oct 17 '13 at 19:40
I understand you answer but I don't know how to continue it. Can you please show $c_{2n−2}$. –  Ilya_Gazman Nov 11 '13 at 8:06
What about RSA-129 –  Ilya_Gazman Nov 28 '13 at 23:41

Extending what @Amir wrote, I came across the following nice web page which hosts a CNF generator for factoring circuits that one could e.g. run on some of the (now inactive) RSA Factoring Challenge numbers. The generated instances are in DIMACS format that can directly be fed to any one of the current competitors in the annual SAT solver competition. Regarding hard SAT instances in general, the benchmark problems given at the SAT competition site appear to be quite useful, also the classification into random/crafted/industrial is nice.

-
That link is very cool! –  Huck Bennett May 28 '11 at 16:23
If you actually try inputting one of those numbers you'll find their source code uses the int datatype and therefore can only hold 32-bit numbers, while the unfactored RSA numbers start at hundreds of bits. –  René G Dec 9 '14 at 3:10

Here's a paper on generating SAT instances from factoring:

Horie, S. & Watanabe, O. [1997] "Hard instance generation for SAT" Algorithms and Computation 1350:22-31 (pdf)

It's worse than linear, but better than $n^2$. A 512-bit RSA challenge type number generates an instance with 63,652 variables and 406,860 clauses.

-

ToughSat by Henry Yuen and Joseph Bebel is another tool similar to the one linked by @Martin, which generates CNF formulas that encode instances of factoring and other hard problems.

-