Re: Integer Factorization with SAT

Thorsten Kiefer wrote:

Torben Ægidius Mogensen wrote:

novice <Tjackson.1982@xxxxxxxxx> 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

.