Integer Factorization with SAT

On Aug 4, 11:40 am, jacko <jackokr...@gmail.com> wrote:
> 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 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- 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




P(x)^Q(x) is not a polynomial. For example, (2)^(5x) is clearly
exponential; that's practically the definition of how to express
exponential time.

-Phil

On 4 Aug, 23:06, cplxp...@gmail.com wrote:
> On Aug 4, 11:40 am, jacko <jackokr...@gmail.com> wrote:
>
>
>
>
>
> > 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 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- 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
>
> P(x)^Q(x) is not a polynomial. *For example, (2)^(5x) is clearly
> exponential; that's practically the definition of how to express
> exponential time.
>
> -Phil- Hide quoted text -
>
> - Show quoted text -

yes but e^x has a infinite polynomial representation

On Aug 4, 7:15 pm, jacko <jackokr...@gmail.com> wrote:
> On 4 Aug, 23:06, cplxp...@gmail.com wrote:
>
>
>
> > On Aug 4, 11:40 am, jacko <jackokr...@gmail.com> wrote:
>
> > > 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 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- 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
>
> > P(x)^Q(x) is not a polynomial. For example, (2)^(5x) is clearly
> > exponential; that's practically the definition of how to express
> > exponential time.
>
> > -Phil- Hide quoted text -
>
> > - Show quoted text -
>
> yes but e^x has a infinite polynomial representation


Perhaps, if you are dealing with the notion of polynomial-boundedness,
that's irrelevant. e^x is not bounded by any finite polynomial.

-Phil

I went down this path and didn't have much luck.

yes with certain situations you can eliminate possibilities, BUT the
longer the (length of the answer) in bits the more possibilities you
will face.

try 11 x 13

This could lead to multiple "possible" multiplication results. Even if
you can solve 2sat in poly time, the heart of the problem is how many
solutions can you find, and then a decision of which one is correct.

Theres Hope! Using what I call imaging or partial view, where if
theres a one in the number, the OTHER number will appear. I'm probably
not explaining this super well, but if you make images a "priority"
choice that could lead to an answer faster.

novice <Tjackson.1982@gmail.com> writes:

> I went down this path and didn't have much luck.
>
> yes with certain situations you can eliminate possibilities, BUT the
> longer the (length of the answer) in bits the more possibilities you
> will face.
>
> try 11 x 13
>
> This could lead to multiple "possible" multiplication results.

You could add constraints that the first number is at least as big as
the other. That is just a linear number of extra constraints.

You also need a constraint that prevents a number from being 1, so you
don't get the trivial "factorisation" n = n*1.

I tried doing this som eyears ago, and found that even with a fairly
good SAT solver, it took way longer to factorise by SAT solving than
by just dividing by all odd numbers up to the square root of n.

This might improve if you use a O(n*log(m)) multiplier "circuit"
instead of the normal O(n*m) schoolbook multiplication, but the higher
constant factor means you need fairly large numbers before you get any
savings. And even then it is doubtful you get anything nearly as fast
as trivial arithmetic methods.

Torben

Torben Ægidius Mogensen wrote:

> novice <Tjackson.1982@gmail.com> writes:
>
>> I went down this path and didn't have much luck.
>>
>> yes with certain situations you can eliminate possibilities, BUT the
>> longer the (length of the answer) in bits the more possibilities you
>> will face.
>>
>> try 11 x 13
>>
>> This could lead to multiple "possible" multiplication results.
>
> You could add constraints that the first number is at least as big as
> the other. That is just a linear number of extra constraints.
>
> You also need a constraint that prevents a number from being 1, so you
> don't get the trivial "factorisation" n = n*1.
Right, I forgot that in the old version. I'll publish a new version
which corrects this....

>
> I tried doing this som eyears ago, and found that even with a fairly
> good SAT solver, it took way longer to factorise by SAT solving than
> by just dividing by all odd numbers up to the square root of n.
right !
This generator is just a proof of concept, not of practical use (yet).

>
> This might improve if you use a O(n*log(m)) multiplier "circuit"
> instead of the normal O(n*m) schoolbook multiplication, but the higher
At a first glance i'd say, O(n*log(m)) would result in a bigger sat
instance, because it needs more conditional logic, right ?
Can you give a schematic algorithm for that multiplication circuit ?

> constant factor means you need fairly large numbers before you get any
> savings. And even then it is doubtful you get anything nearly as fast
> as trivial arithmetic methods.
>
> Torben

-Thorsten

Thorsten Kiefer wrote:

> Torben Ægidius Mogensen wrote:
>
>> novice <Tjackson.1982@gmail.com> writes:
>>
>>> I went down this path and didn't have much luck.
>>>
>>> yes with certain situations you can eliminate possibilities, BUT the
>>> longer the (length of the answer) in bits the more possibilities you
>>> will face.
>>>
>>> try 11 x 13
>>>
>>> This could lead to multiple "possible" multiplication results.
>>
>> You could add constraints that the first number is at least as big as
>> the other. That is just a linear number of extra constraints.
>>
>> You also need a constraint that prevents a number from being 1, so you
>> don't get the trivial "factorisation" n = n*1.
> Right, I forgot that in the old version. I'll publish a new version
> which corrects this....

I uploaded a new version. It also corrects the pythagoras and fermat
generators.

>
>>
>> I tried doing this som eyears ago, and found that even with a fairly
>> good SAT solver, it took way longer to factorise by SAT solving than
>> by just dividing by all odd numbers up to the square root of n.
> right !
> This generator is just a proof of concept, not of practical use (yet).
>
>>
>> This might improve if you use a O(n*log(m)) multiplier "circuit"
>> instead of the normal O(n*m) schoolbook multiplication, but the higher
> At a first glance i'd say, O(n*log(m)) would result in a bigger sat
> instance, because it needs more conditional logic, right ?
> Can you give a schematic algorithm for that multiplication circuit ?
>
>> constant factor means you need fairly large numbers before you get any
>> savings. And even then it is doubtful you get anything nearly as fast
>> as trivial arithmetic methods.
>>
>> Torben
>
> -Thorsten

Thorsten Kiefer <webmaster@tokisworld.org> writes:

> Torben Ægidius Mogensen wrote:

>> This might improve if you use a O(n*log(m)) multiplier "circuit"
>> instead of the normal O(n*m) schoolbook multiplication, but the higher
> At a first glance i'd say, O(n*log(m)) would result in a bigger sat
> instance, because it needs more conditional logic, right ?

Not really. The O(n*log(m)) multiplier is a static network based on
FFT.

> Can you give a schematic algorithm for that multiplication circuit ?

http://en.wikipedia.org/wiki/Sch%C3%...ssen_algorithm

Note that you need quite large numbers before this algorithm pays off,
so you might want to use
http://en.wikipedia.org/wiki/Karatsuba_algorithm instead, which wins
over classical schoolbook multiplication on fairly small numbers.

Note that for SAT, you want to reduce the number of binary variables
involved, but adding extra constraints has little cost -- in fact,
more constraints may get you a solution faster.

Torben