Hi, I have uploaded some new SAT instances based on hardness of
factoring the product of two large prime numbers, n=pq. These
instances are always satisfiable.
The instances are in files named 'xbits.dimacs' where x denotes the
bitlength of n. I did not attach the p,q for each, but can do so at
request. I can also generate many more instances easily.
These instances were generated by myself, based on the ToughSAT
project (by myself and Henry Yuen) but with a substantially revised
and new generator I wrote for 2015 which makes far smaller factoring
instances out of any given pair of primes (smaller than our previous
generator). This new generator generates new instances based on
Karatsuba multiplication.
Joe Bebel