Re: Integer Factorization with SAT

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.

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
.