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?