| View previous topic :: View next topic |
| Author |
Message |
Thorsten Kiefer
Guest
|
 Posted: Wed Jul 30, 2008 6:59 am Post subject: 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 |
|
| |
|
 Back to top |
Thorsten Kiefer
Guest
|
| Posted: Wed Jul 30, 2008 7:00 am Post subject: Re: Integer Factorization with SAT |
|
|
Thorsten Kiefer wrote:
[quote]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
[/quote]
you can start it with java -jar SATConverter.jar |
|
| |
|
| Back to top |
jacko
Guest
|
| Posted: Wed Jul 30, 2008 10:15 pm Post subject: Re: Integer Factorization with SAT |
|
|
On 30 Jul, 03:00, Thorsten Kiefer <webmas...@tokisworld.org> wrote:
[quote]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
[/quote]
What>s a SAT? http://mid4th.googlecode.com is i worth converting to a
phone MIDlet? |
|
| |
|
| Back to top |
Guest
|
| Posted: Wed Jul 30, 2008 10:53 pm Post subject: Re: Integer Factorization with SAT |
|
|
On Jul 30, 6:15 pm, jacko <jackokr...@gmail.com> wrote:
[quote]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?
[/quote]
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 |
|
| |
|
| Back to top |
Thorsten Kiefer
Guest
|
| Posted: Thu Jul 31, 2008 1:32 pm Post subject: Re: Integer Factorization with SAT |
|
|
cplxphil@gmail.com wrote:
[quote]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 ;))[/quote]
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......
[quote]
This is a pretty sweet application though. Thanks for making it!
Thanks ;)))
-Phil
-Thorsten[/quote] |
|
| |
|
| Back to top |
Guest
|
| Posted: Thu Jul 31, 2008 9:07 pm Post subject: Re: Integer Factorization with SAT |
|
|
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 |
|
| |
|
| Back to top |
Guest
|
| Posted: Fri Aug 01, 2008 2:57 am Post subject: Re: Integer Factorization with SAT |
|
|
On Jul 31, 7:24 pm, Thorsten Kiefer <webmas...@tokisworld.org> wrote:
[quote]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
[/quote]
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 |
|
| |
|
| Back to top |
Thorsten Kiefer
Guest
|
| Posted: Fri Aug 01, 2008 4:24 am Post subject: Re: Integer Factorization with SAT |
|
|
cplxphil@gmail.com wrote:
[quote]
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
[/quote]
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 |
|
| |
|
| Back to top |
|
