Re: reducing the factorization decision problem to SAT?
- From: djimenez@xxxxxxxxxxxxx (Daniel A. Jimenez)
- Date: 16 Jul 2008 19:09:03 -0500
In article <911283c4-67f6-4bb9-8c4c-91cdcd9bec8a@xxxxxxxxxxxxxxxxxxxxxxxxxxxx>,
<cplxphil@xxxxxxxxx> wrote:
On Jul 16, 6:28 pm, djime...@xxxxxxxxxxxxx (Daniel A. Jimenez) wrote:
In article <73f0758f-8c5b-4682-803e-c509edcd9...@xxxxxxxxxxxxxxxxxxxxxxxxxxxx>,
<cplxp...@xxxxxxxxx> wrote:
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
Suppose you want to find a factor of a positive integer n and all you
have is SAT. Construct a combinational circuit that multiplies two binary
numbers, a and b, resulting in a binary number c[1..k] where k is at least
ceil(log_2(n)). Then assert logically that c is equal to n, e.g. make
a k-input AND gate for which the i'th input is c[i] if n[i] is 1, or NOT
c[i] if n[i] is 0, and then assert that the output of this AND gate is 1.
That is, the output of the whole circuit is the output of this AND gate,
and it will only be 1 if a and b are factors of n. Convert this circuit
into CNF-SAT (a subset of general SAT) using the construction you can find
in CLRS, or if you type "to CNF efficiently" as a Google Groups search to
find a post I made a few years ago. The resulting formula is satisfiable
only by values of a and b that are factors of n. If all you have is
something that decides SAT without providing satisfying assignments,
just go setting subsequent bits of a and b to 0 and 1, asking whether
the formula is still satisfiable and keeping values for which the formula
remains satisfiable. This is a little different from the decision problem
formulation of factorization you mention but the result is the same.
I think that is similar to the Cook-Levin mapping, isn't it? The
alternate version that deals with circuits instead of Turing
machines is what yours sounds like.
Is there any simpler algorithm, or is that the best that can be done?
I'm looking for the sort of algorithm that I would actually know how
to program in C++...
Thanks for the reply...I figure that is probably the best that can be
done. I wish that there were a simpler reduction.
-Phil
I think this is as simple as it gets. I've coded this a couple of times and
I don't think it's too difficult if you've got a reasonable CS background.
First code a binary multiplication algorithm using arrays of Boolean values
for numbers. You could use the grade-school multiplication algorithm in
base 2 and ripple-carry addition to add the partial products. Test it to
make sure it works, then substitute some kind of gate data structure for the
Booleans so that e.g. instead of having "a AND b" return a value, it turns
into an AND gate with pointers to a and b. The input to the algorithm,
rather than being particular Boolean values, are special "input" gates.
So instead of the multiplication algorithm actually multiplying numbers,
it generates a DAG from these gates that ends up being your circuit.
Add in a few more gates to do the k-input AND gate for your value of n
and you're all done.
--
Daniel Jimenez djimenez@xxxxxxxxxxxxx
"I've so much music in my head" -- Maurice Ravel, shortly before his death.
" " -- John Cage
.
- References:
- reducing the factorization decision problem to SAT?
- From: cplxphil
- Re: reducing the factorization decision problem to SAT?
- From: Daniel A. Jimenez
- Re: reducing the factorization decision problem to SAT?
- From: cplxphil
- reducing the factorization decision problem to SAT?
- Prev by Date: Re: reducing the factorization decision problem to SAT?
- Next by Date: moving pairs
- Previous by thread: Re: reducing the factorization decision problem to SAT?
- Next by thread: moving pairs
- Index(es):
Relevant Pages
|
