| View previous topic :: View next topic |
| Author |
Message |
Guest
|
 Posted: Fri Jul 18, 2008 8:45 pm Post subject: Integer factorization reduction to SAT |
 |
|
Hello,
Does anyone know if there is in existence an already-programmed
executable (for Windows, preferably) that reduces an instance of the
integer factorization problem to an instance of SAT? I posted on here
a while ago asking how to perform such a reduction, and someone was
kind enough to answer, but I do not know how to perform the reduction
myself. If anyone knows the location of any such program, I would
really appreciate it if someone could point me in the direction of
it. (There is something resembling one here (http://
www.is.titech.ac.jp/~watanabe/gensat/a2/), but it doesn>t seem to
allow the user to enter a single integer and reduce the identity of
one of its factors to a decision problem.)
If anyone can help I>d really appreciate it.
-Phil |
|
| |
|
 Back to top |
Guest
|
| Posted: Fri Jul 18, 2008 11:47 pm Post subject: Re: Integer factorization reduction to SAT |
|
|
On Jul 18, 7:22 pm, Thorsten Kiefer <m...@home.org> wrote:
[quote]Thorsten Kiefer wrote:
cplxp...@gmail.com wrote:
Hello,
Does anyone know if there is in existence an already-programmed
executable (for Windows, preferably) that reduces an instance of the
integer factorization problem to an instance of SAT? I posted on here
a while ago asking how to perform such a reduction, and someone was
kind enough to answer, but I do not know how to perform the reduction
myself. If anyone knows the location of any such program, I would
really appreciate it if someone could point me in the direction of
it. (There is something resembling one here (http://
www.is.titech.ac.jp/~watanabe/gensat/a2/), but it doesn>t seem to
allow the user to enter a single integer and reduce the identity of
one of its factors to a decision problem.)
If anyone can help I>d really appreciate it.
-Phil
Hi,
a rough outline of the reduction is that :
we assume x = a*b, and a =a0a1a2a3...an,b=b0b1b2...bn
x=x0x1x2...x2n
Now create a non recurrent logic circuit of that multiplication.
then convert that logic circuit to sat.
assert x0,x1,x2...x2n to the correspondintg bits of the integer to be
factorized.
then start your favorite sat solver.
then extract a0,a1...an,b0,b1,...bn.
TK
Hi,
have a look at this :http://tokisworld.org/sat/dtest.tbz
Maybe this helps you a bit.
I>ll see if I can write a factor-to-sat converter.
TK
[/quote]
I couldn>t open that link. I>m running Windows, could that be it?
If you>d actually go to the trouble of writing that for me, I>d really
really appreciate it. That>s very nice of you.
-Phil |
|
| |
|
| Back to top |
Thorsten Kiefer
Guest
|
| Posted: Sat Jul 19, 2008 3:55 am Post subject: Re: Integer factorization reduction to SAT |
|
|
cplxphil@gmail.com wrote:
[quote]
Hello,
Does anyone know if there is in existence an already-programmed
executable (for Windows, preferably) that reduces an instance of the
integer factorization problem to an instance of SAT? I posted on here
a while ago asking how to perform such a reduction, and someone was
kind enough to answer, but I do not know how to perform the reduction
myself. If anyone knows the location of any such program, I would
really appreciate it if someone could point me in the direction of
it. (There is something resembling one here (http://
www.is.titech.ac.jp/~watanabe/gensat/a2/), but it doesn>t seem to
allow the user to enter a single integer and reduce the identity of
one of its factors to a decision problem.)
If anyone can help I>d really appreciate it.
-Phil
[/quote]
Hi,
I did it once, but I must search for the code.
would you be interested in a rijndael-to-sat reduction ?
Regards
TK |
|
| |
|
| Back to top |
Thorsten Kiefer
Guest
|
| Posted: Sat Jul 19, 2008 4:03 am Post subject: Re: Integer factorization reduction to SAT |
|
|
cplxphil@gmail.com wrote:
[quote]
Hello,
Does anyone know if there is in existence an already-programmed
executable (for Windows, preferably) that reduces an instance of the
integer factorization problem to an instance of SAT? I posted on here
a while ago asking how to perform such a reduction, and someone was
kind enough to answer, but I do not know how to perform the reduction
myself. If anyone knows the location of any such program, I would
really appreciate it if someone could point me in the direction of
it. (There is something resembling one here (http://
www.is.titech.ac.jp/~watanabe/gensat/a2/), but it doesn>t seem to
allow the user to enter a single integer and reduce the identity of
one of its factors to a decision problem.)
If anyone can help I>d really appreciate it.
-Phil
[/quote]
Hi,
a rough outline of the reduction is that :
we assume x = a*b, and a =a0a1a2a3...an,b=b0b1b2...bn
x=x0x1x2...x2n
Now create a non recurrent logic circuit of that multiplication.
then convert that logic circuit to sat.
assert x0,x1,x2...x2n to the correspondintg bits of the integer to be
factorized.
then start your favorite sat solver.
then extract a0,a1...an,b0,b1,...bn.
TK |
|
| |
|
| Back to top |
Thorsten Kiefer
Guest
|
| Posted: Sat Jul 19, 2008 4:22 am Post subject: Re: Integer factorization reduction to SAT |
|
|
Thorsten Kiefer wrote:
[quote]cplxphil@gmail.com wrote:
Hello,
Does anyone know if there is in existence an already-programmed
executable (for Windows, preferably) that reduces an instance of the
integer factorization problem to an instance of SAT? I posted on here
a while ago asking how to perform such a reduction, and someone was
kind enough to answer, but I do not know how to perform the reduction
myself. If anyone knows the location of any such program, I would
really appreciate it if someone could point me in the direction of
it. (There is something resembling one here (http://
www.is.titech.ac.jp/~watanabe/gensat/a2/), but it doesn>t seem to
allow the user to enter a single integer and reduce the identity of
one of its factors to a decision problem.)
If anyone can help I>d really appreciate it.
-Phil
Hi,
a rough outline of the reduction is that :
we assume x = a*b, and a =a0a1a2a3...an,b=b0b1b2...bn
x=x0x1x2...x2n
Now create a non recurrent logic circuit of that multiplication.
then convert that logic circuit to sat.
assert x0,x1,x2...x2n to the correspondintg bits of the integer to be
factorized.
then start your favorite sat solver.
then extract a0,a1...an,b0,b1,...bn.
TK
[/quote]
Hi,
have a look at this : http://tokisworld.org/sat/dtest.tbz
Maybe this helps you a bit.
I>ll see if I can write a factor-to-sat converter.
TK |
|
| |
|
| Back to top |
|
