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?