Re: Integer Factorization with SAT

cplxphil@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


.

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
    ... 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 ... though...maybe this exponential time situation could ...
    (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, ... naive (much like most of my approaches to proving P!= NP, ... So I don't really have any good ideas for making a polynomial time SAT ... whether you're investigating a true statement or the "world" ...
    (comp.theory)