11
$\begingroup$

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?

Improve this question
$\endgroup$

1 Answer 1

Reset to default
10
$\begingroup$

There are other much simpler instances which we provably know that the current algorithms cannot solve in sub-exponential time. These algorithms are incapable of counting (almost all of them are improvements of DPLL which correspond to Resolution propositional proof system).

Unfortunately such examples are unsatisfiable instances. The question about finding natural satisfiable hard instances for these algorithms is an interesting research problem (Russell Impagliazzo mentioned this during the proof complexity workshop last year at Banff). There are satisfiable instances that we provably know the algorithms fail badly if there is any such instance, but they are not very natural (they are based on formulas expressing the soundness of algorithms).

Regarding factoring, if the size of numbers are small (e.g. logarithmic as in your case, i.e. the numbers are given in unary), then theoretically there is no result that says there cannot be solved by current algorithms, and in fact we can write simple polynomial time algorithms that factor these numbers. So whether a particular SAT solver program can solve them might depend on the particular algorithm.

Improve this answer
$\endgroup$
5
  • $\begingroup$ 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? $\endgroup$
    – Artem Kaznatcheev
    Jul 22, 2012 at 6:04
  • $\begingroup$ @Artem, any proof complexity lowerbound for Resolution would give an example, take for example pigeon hole principle. One can easily extract a Resolution (refutation) proof for the unsatisfiable instance from the computation of these algorithms on that instance. There was a nice survey by Nathan Segerlind from 2007 that IIRC covers this among other things. Let me know if it is not there and I will find you another reference. $\endgroup$
    – Kaveh
    Jul 22, 2012 at 6:10
  • $\begingroup$ @Artem, I think the argument works also in the case that just one of the numbers is logarithmic, i.e. we can solve it in polynomial time by going over all small numbers to see if one of them is a factor of the product. $\endgroup$
    – Kaveh
    Jul 22, 2012 at 6:12
  • $\begingroup$ @Kaven yes, that is why I made one of the number logarithmic in size. I explain it in the question. I just don't want an answer that assumes unary representation as your 3rd paragraph suggested. I will take a look at Segerlind later. Once again, thanks for the comment :D. $\endgroup$
    – Artem Kaznatcheev
    Jul 22, 2012 at 6:15
  • $\begingroup$ @Artem, you are welcome. :) (I used unary because I assumed that both numbers are small and used being unary to deal with the fact that the size should be exponential in them, alternatively one can just pad to make them big.) $\endgroup$
    – Kaveh
    Jul 22, 2012 at 6:17

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.