Prev: Example for a non-rec.enum. language whose complement isn't rec.enum., too.
Next: halting problem proof, via diagonalization?
From: cplxphil on 18 Jul 2008 16:45

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
From: Thorsten Kiefer on 18 Jul 2008 18:55
cplxphil(a)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,
I did it once, but I must search for the code.
would you be interested in a rijndael-to-sat reduction ?

Regards
TK
From: Thorsten Kiefer on 18 Jul 2008 19:03
cplxphil(a)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
From: Thorsten Kiefer on 18 Jul 2008 19:22
Thorsten Kiefer wrote:

> cplxphil(a)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

From: cplxphil on 18 Jul 2008 19:47
On Jul 18, 7:22 pm, Thorsten Kiefer <m...(a)home.org> wrote:
> Thorsten Kiefer wrote:
> > cplxp...(a)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


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
 | 
Pages: 1
Prev: Example for a non-rec.enum. language whose complement isn't rec.enum., too.
Next: halting problem proof, via diagonalization?