Re: Integer Factorization with SAT

On Jul 31, 7:24 pm, Thorsten Kiefer <webmas...@xxxxxxxxxxxxxx> wrote:
cplxp...@xxxxxxxxx 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

.

Relevant Pages

  • Re: Integer Factorization with SAT
    ... whether you're investigating a true statement or the "world" ... I use siege_v4 - the fastest solver i know..... ... Now the question is "is there a sequence for the multiplications ... i.e. the product of two polynomials is itself a polynomial. ...
    (comp.theory)
  • Re: Integer Factorization with SAT
    ... I use siege_v4 - the fastest solver i know..... ... Now the question is "is there a sequence for the multiplications ... though...maybe this exponential time situation could ... i.e. the product of two polynomials is itself a polynomial. ...
    (comp.theory)
  • Re: Integer Factorization with SAT
    ... whether you're investigating a true statement or the "world" ... I use siege_v4 - the fastest solver i know..... ... Now the question is "is there a sequence for the multiplications ... i.e. the product of two polynomials is itself a polynomial. ...
    (comp.theory)
  • Re: Integer Factorization with SAT
    ... whether you're investigating a true statement or the "world" ... I use siege_v4 - the fastest solver i know..... ... Now the question is "is there a sequence for the multiplications ... i.e. the product of two polynomials is itself a polynomial.. ...
    (comp.theory)
  • Re: Integer Factorization with SAT
    ... I did have the intention of writing a SAT solver, ... whether you're investigating a true statement or the "world" ... Now the question is "is there a sequence for the multiplications ... Once I found a sorting algorithm with wich ...
    (comp.theory)