reducing the factorization decision problem to SAT?

Hi,

It's obviously possible to reduce an NP decision problem to SAT using
Cook-Levin's mapping, but how does one do it in an "intelligible,"
simple way in practice for integer factorization?

I know it's been done before, I just don't know how. Specifically,
how do you reduce this decision problem...

Given an integer n and an integer k s.t. 1 < k < n, are there any
integers j s.t. j divides n and 1 < j < k?

....to SAT? (Or any other decision problem that the factorization
problem can be Turing reduced to? I suppose that simply asking if
there are any nontrivial factors (i.e., not equal to +/-1 or +/-n)
would work just as well.) If anyone knows how to reduce factorization
to SAT I'd be interested to know how it's done.

Thanks,

Phil
.

Relevant Pages

  • Re: reducing the factorization decision problem to SAT?
    ... It's obviously possible to reduce an NP decision problem to SAT using ... (Or any other decision problem that the factorization ... That is, the output of the whole circuit is the output of this AND gate, ... something that decides SAT without providing satisfying assignments, ...
    (comp.theory)
  • factorization an NP problem (dont see it)
    ... factorization as a decision problem: given a composite integer m and ... if this can be done for all intergers upto k in polynomial time O, ...
    (sci.math)