# Can top SAT-solvers factor easy numbers?

Modern SAT-solvers are very good at solving many real-world examples of SAT instances. However, we know how to generate hard ones: for instance use a reduction from factoring to SAT and give the RSA numbers as input.

This raises the question: what if I take an easy example of factoring. Instead of taking two large primes on $n/2$ bits, what if I take a prime $p$ on $\log n$ bits and a prime q on $n/\log n$ bits, let $N = pq$ and the encode $\mathrm{FACTOR}(N)$ as a SAT instance. $N$ would be an easy number to factor by brute-force search or sieve methods since one of the factors in so small; does a modern SAT-solver with some standard reduction from factoring to SAT also pick up on this structure?

Can top SAT-solvers factor $N = pq$ where $|p| = \log n$ quickly?

• I was hoping to use binary and just have one of the factors to be very small (on the order $\log N$, while the other is $N/\log N$) to preserve as much as possible of normal factoring (I feel like switching to unary just changes too many things for me). Thanks for the info on simpler problems, can you provide a link to a paper about the hard unsatisfiable instances based on counting? – Artem Kaznatcheev Jul 22 '12 at 6:04