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
.

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 ... though...maybe this exponential time situation could ...
    (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)