Integer Factorization with SAT

Hi,
I wanna announce my little program, which
reduces the factorization problem into a sat instance.

http://tokisworld.org/sat/SATConverter.jar

Have fun with it !!!

-Thorsten

Thorsten Kiefer wrote:

> Hi,
> I wanna announce my little program, which
> reduces the factorization problem into a sat instance.
>
> http://tokisworld.org/sat/SATConverter.jar
>
> Have fun with it !!!
>
> -Thorsten

you can start it with java -jar SATConverter.jar

On 30 Jul, 03:00, Thorsten Kiefer <webmas...@tokisworld.org> wrote:
> Thorsten Kiefer wrote:
> > Hi,
> > I wanna announce my little program, which
> > reduces the factorization problem into a sat instance.
>
> >http://tokisworld.org/sat/SATConverter.jar
>
> > Have fun with it !!!
>
> > -Thorsten
>
> you can start it with java -jar SATConverter.jar

What's a SAT? http://mid4th.googlecode.com is i worth converting to a
phone MIDlet?

On Jul 30, 6:15 pm, jacko <jackokr...@gmail.com> wrote:
> On 30 Jul, 03:00, Thorsten Kiefer <webmas...@tokisworld.org> wrote:
>
> > Thorsten Kiefer wrote:
> > > Hi,
> > > I wanna announce my little program, which
> > > reduces the factorization problem into a sat instance.
>
> > >http://tokisworld.org/sat/SATConverter.jar
>
> > > Have fun with it !!!
>
> > > -Thorsten
>
> > you can start it with java -jar SATConverter.jar
>
> What's a SAT?http://mid4th.googlecode.comis i worth converting to a
> phone MIDlet?


SAT is a decision problem relevant to complexity theory. I don't
think it would have much of a market, nor would it be terribly useful
on a cell phone.

This is a pretty sweet application though. Thanks for making it!

-Phil

cplxphil@gmail.com wrote:

> On Jul 30, 6:15 pm, jacko <jackokr...@gmail.com> wrote:
>> On 30 Jul, 03:00, Thorsten Kiefer <webmas...@tokisworld.org> wrote:
>>
>> > Thorsten Kiefer wrote:
>> > > Hi,
>> > > I wanna announce my little program, which
>> > > reduces the factorization problem into a sat instance.
>>
>> > >http://tokisworld.org/sat/SATConverter.jar
>>
>> > > Have fun with it !!!
>>
>> > > -Thorsten
>>
>> > you can start it with java -jar SATConverter.jar
>>
>> What's a SAT?http://mid4th.googlecode.comis i worth converting to a
>> phone MIDlet?
>
>
> SAT is a decision problem relevant to complexity theory. I don't
> think it would have much of a market, nor would it be terribly useful
> on a cell phone.
If you can write a polynomial sat solver, it will have much of a market )
Actually that's the point ! I wrote this converter once, because I wanted
to write a good sat solver. And randomly generated sat instances are too
easy to solve. I would roughly guess that you have the same intention ?!?
I have some (stupid???) ideas for a sat solver. If you want, I can share
them with you......
>
> This is a pretty sweet application though. Thanks for making it!
Thanks ))
>
> -Phil
-Thorsten

I did have the intention of writing a SAT solver, but my approach was
naive (much like most of my approaches to proving P != NP, also...).
I thought that it was easy to decide the language TAUTOLOGY because I
made the (false) assumption that it's possible to convert any formula
to conjunctive normal form in polynomial time.

So I don't really have any good ideas for making a polynomial time SAT
solver...I'm more interested in trying to prove P != NP at this point,
since that seems more probably anyway.

Nonetheless, it would be interesting to hear your ideas for solving
SAT if you'd like to share them. My amateur but I think correct
opinion is that any insight you can get into a difficult problem is
useful, whether you're investigating a true statement or the "world"
in which a true statement is false (it should give rise to a
contradiction). In other words, I think it could be useful to
understanding why P != NP if we investigate methods for trying to
prove P = NP is true.

-Phil

cplxphil@gmail.com wrote:

>
> I did have the intention of writing a SAT solver, but my approach was
> naive (much like most of my approaches to proving P != NP, also...).
> I thought that it was easy to decide the language TAUTOLOGY because I
> made the (false) assumption that it's possible to convert any formula
> to conjunctive normal form in polynomial time.
>
> So I don't really have any good ideas for making a polynomial time SAT
> solver...I'm more interested in trying to prove P != NP at this point,
> since that seems more probably anyway.
>
> Nonetheless, it would be interesting to hear your ideas for solving
> SAT if you'd like to share them. My amateur but I think correct
> opinion is that any insight you can get into a difficult problem is
> useful, whether you're investigating a true statement or the "world"
> in which a true statement is false (it should give rise to a
> contradiction). In other words, I think it could be useful to
> understanding why P != NP if we investigate methods for trying to
> prove P = NP is true.
>
> -Phil

Hi,
I updated the jar file !! Have a look at it !!!!
Which solver do you use at the moment ?
I use siege_v4 - the fastest solver i know.....

My approach for a SAT solver was pretty simple :
Simply multiply everything out.
One would say that we get exponentially many terms,
but boolean simplifications reduce the number of terms
in the intermediate results.
Now the question is "is there a sequence for the multiplications
which does not produce exponentially many terms ??"

I tried to sort the MaxTerms in many different ways before
multiplication. Once I found a sorting algorithm with wich
my "multiplying solver" was faster than any other solver on satlib.org.
But that held true only for one single instance.
As it didnt work for the other instrances from satlib.org, i deleted the
code. And now I cannot reproduce that sorting algorithm ((((((

-Thorsten

On Jul 31, 7:24 pm, Thorsten Kiefer <webmas...@tokisworld.org> wrote:
> cplxp...@gmail.com wrote:
>
> > I did have the intention of writing a SAT solver, but my approach was
> > naive (much like most of my approaches to proving P != NP, also...).
> > I thought that it was easy to decide the language TAUTOLOGY because I
> > made the (false) assumption that it's possible to convert any formula
> > to conjunctive normal form in polynomial time.
>
> > So I don't really have any good ideas for making a polynomial time SAT
> > solver...I'm more interested in trying to prove P != NP at this point,
> > since that seems more probably anyway.
>
> > Nonetheless, it would be interesting to hear your ideas for solving
> > SAT if you'd like to share them. My amateur but I think correct
> > opinion is that any insight you can get into a difficult problem is
> > useful, whether you're investigating a true statement or the "world"
> > in which a true statement is false (it should give rise to a
> > contradiction). In other words, I think it could be useful to
> > understanding why P != NP if we investigate methods for trying to
> > prove P = NP is true.
>
> > -Phil
>
> Hi,
> I updated the jar file !! Have a look at it !!!!
> Which solver do you use at the moment ?
> I use siege_v4 - the fastest solver i know.....
>
> My approach for a SAT solver was pretty simple :
> Simply multiply everything out.
> One would say that we get exponentially many terms,
> but boolean simplifications reduce the number of terms
> in the intermediate results.
> Now the question is "is there a sequence for the multiplications
> which does not produce exponentially many terms ??"
>
> I tried to sort the MaxTerms in many different ways before
> multiplication. Once I found a sorting algorithm with wich
> my "multiplying solver" was faster than any other solver on satlib.org.
> But that held true only for one single instance.
> As it didnt work for the other instrances from satlib.org, i deleted the
> code. And now I cannot reproduce that sorting algorithm ((((((
>
> -Thorsten


Hey,

I think that even if some of the terms simplify, you will definitely
be dealing with exponential time. Unless you can prove a polynomial
upper bound on the running time, it's probably not going to work.

It's interesting, though...maybe this exponential time situation could
be used to prove P != NP somehow? I don't really know.

-Phil

On 1 Aug, 03:57, cplxp...@gmail.com wrote:
> On Jul 31, 7:24 pm, Thorsten Kiefer <webmas...@tokisworld.org> wrote:
>
>
>
>
>
> > cplxp...@gmail.com wrote:
>
> > > I did have the intention of writing a SAT solver, but my approach was
> > > naive (much like most of my approaches to proving P != NP, also...)..
> > > I thought that it was easy to decide the language TAUTOLOGY because I
> > > made the (false) assumption that it's possible to convert any formula
> > > to conjunctive normal form in polynomial time.
>
> > > So I don't really have any good ideas for making a polynomial time SAT
> > > solver...I'm more interested in trying to prove P != NP at this point,
> > > since that seems more probably anyway.
>
> > > Nonetheless, it would be interesting to hear your ideas for solving
> > > SAT if you'd like to share them. *My amateur but I think correct
> > > opinion is that any insight you can get into a difficult problem is
> > > useful, whether you're investigating a true statement or the "world"
> > > in which a true statement is false (it should give rise to a
> > > contradiction). *In other words, I think it could be useful to
> > > understanding why P != NP if we investigate methods for trying to
> > > prove P = NP is true.
>
> > > -Phil
>
> > Hi,
> > I updated the jar file !! Have a look at it !!!!
> > Which solver do you use at the moment ?
> > I use siege_v4 - the fastest solver i know.....
>
> > My approach for a SAT solver was pretty simple :
> > Simply multiply everything out.
> > One would say that we get exponentially many terms,
> > but boolean simplifications reduce the number of terms
> > in the intermediate results.
> > Now the question is "is there a sequence for the multiplications
> > which does not produce exponentially many terms ??"
>
> > I tried to sort the MaxTerms in many different ways before
> > multiplication. Once I found a sorting algorithm with wich
> > my "multiplying solver" was faster than any other solver on satlib.org.
> > But that held true only for one single instance.
> > As it didnt work for the other instrances from satlib.org, i deleted the
> > code. And now I cannot reproduce that sorting algorithm ((((((
>
> > -Thorsten
>
> Hey,
>
> I think that even if some of the terms simplify, you will definitely
> be dealing with exponential time. *Unless you can prove a polynomial
> upper bound on the running time, it's probably not going to work.
>
> It's interesting, though...maybe this exponential time situation could
> be used to prove P != NP somehow? *I don't really know.
>
> -Phil- Hide quoted text -
>
> - Show quoted text -

from my point of view P!=NP is due to the way that ploynomials can be
producted, i.e. the product of two polynomials is itself a polynomial.
But we have P(x)^Q(x) = ? is this a polynomial?

cheers
jacko

On 4 Aug, 16:31, jacko <jackokr...@gmail.com> wrote:
> On 1 Aug, 03:57, cplxp...@gmail.com wrote:
>
>
>
>
>
> > On Jul 31, 7:24 pm, Thorsten Kiefer <webmas...@tokisworld.org> wrote:
>
> > > cplxp...@gmail.com wrote:
>
> > > > I did have the intention of writing a SAT solver, but my approach was
> > > > naive (much like most of my approaches to proving P != NP, also....).
> > > > I thought that it was easy to decide the language TAUTOLOGY becauseI
> > > > made the (false) assumption that it's possible to convert any formula
> > > > to conjunctive normal form in polynomial time.
>
> > > > So I don't really have any good ideas for making a polynomial time SAT
> > > > solver...I'm more interested in trying to prove P != NP at this point,
> > > > since that seems more probably anyway.
>
> > > > Nonetheless, it would be interesting to hear your ideas for solving
> > > > SAT if you'd like to share them. *My amateur but I think correct
> > > > opinion is that any insight you can get into a difficult problem is
> > > > useful, whether you're investigating a true statement or the "world"
> > > > in which a true statement is false (it should give rise to a
> > > > contradiction). *In other words, I think it could be useful to
> > > > understanding why P != NP if we investigate methods for trying to
> > > > prove P = NP is true.
>
> > > > -Phil
>
> > > Hi,
> > > I updated the jar file !! Have a look at it !!!!
> > > Which solver do you use at the moment ?
> > > I use siege_v4 - the fastest solver i know.....
>
> > > My approach for a SAT solver was pretty simple :
> > > Simply multiply everything out.
> > > One would say that we get exponentially many terms,
> > > but boolean simplifications reduce the number of terms
> > > in the intermediate results.
> > > Now the question is "is there a sequence for the multiplications
> > > which does not produce exponentially many terms ??"
>
> > > I tried to sort the MaxTerms in many different ways before
> > > multiplication. Once I found a sorting algorithm with wich
> > > my "multiplying solver" was faster than any other solver on satlib.org.
> > > But that held true only for one single instance.
> > > As it didnt work for the other instrances from satlib.org, i deleted the
> > > code. And now I cannot reproduce that sorting algorithm ((((((
>
> > > -Thorsten
>
> > Hey,
>
> > I think that even if some of the terms simplify, you will definitely
> > be dealing with exponential time. *Unless you can prove a polynomial
> > upper bound on the running time, it's probably not going to work.
>
> > It's interesting, though...maybe this exponential time situation could
> > be used to prove P != NP somehow? *I don't really know.
>
> > -Phil- Hide quoted text -
>
> > - Show quoted text -
>
> from my point of view P!=NP is due to the way that ploynomials can be
> producted, i.e. the product of two polynomials is itself a polynomial.
> But we have P(x)^Q(x) = ? is this a polynomial?
>
> cheers
> jacko- Hide quoted text -
>
> - Show quoted text -

Binomial theorem would suggest yes! but radius of convergence problem
wold suggest bounds! so its the summation problem?

cheers
jacko

wikipedia.org Ringfield mathematics ("/" = not swap "*")

http://nibz.googlecode.com