Integer factorization using Z3 SMT solver

(The following text has been moved to the article at https://yurichev.com/tmp/SAT_SMT_DRAFT.pdf.)

Integer factorization is method of breaking a composite (non-prime number) into prime factors. Like 12345 = 3*4*823.

Though for small numbers, this task can be accomplished by Z3:

#!/usr/bin/env python

# note: there is no primality test at all, no lookup tables, etc

import random
from z3 import *
from operator import mul

def factor(n):
    print "factoring",n

    in1,in2,out=Ints('in1 in2 out')

    s=Solver()
    s.add(out==n)
    s.add(in1*in2==out)
    # inputs cannot be negative and must be non-1:
    s.add(in1>1)
    s.add(in2>1)

    if s.check()==unsat:
        print n,"is prime (unsat)"
        return [n]
    if s.check()==unknown:
        print n,"is probably prime (unknown)"
        return [n]

    m=s.model()
    # get inputs of multiplier:
    in1_n=m[in1].as_long()
    in2_n=m[in2].as_long()

    print "factors of", n, "are", in1_n, "and", in2_n
    # factor factors recursively:
    rt=sorted(factor (in1_n) + factor (in2_n))
    # self-test:
    assert reduce(mul, rt, 1)==n
    return rt

# infinite test:
def test():
    while True:
        print factor (random.randrange(1000000000))

#test()

# tested by Mathematica:
#print factor(123456) # {{2, 6}, {3, 1}, {643, 1}} 
#print factor(256)
#print factor(999999) # {{3, 3}, {7, 1}, {11, 1}, {13, 1}, {37, 1}}
print factor(1234567890) # {{2, 1}, {3, 2}, {5, 1}, {3607, 1}, {3803, 1}}
#print factor(10000) # {{2, 4}, {5, 4}}
#print factor(123456789012345)
#print factor(3*7*11*17*23*29*31*37*41)
#print factor(1234567890123)
#print factor(2147713027)
#print factor(137446031423)

( The source code: https://github.com/dennis714/yurichev.com/blob/master/blog/factor/factor_z3.py )

When factoring 1234567890 recursively:

% time python z.py
factoring 1234567890
factors of 1234567890 are 342270 and 3607
factoring 342270
factors of 342270 are 2 and 171135
factoring 2
2 is prime (unsat)
factoring 171135
factors of 171135 are 3803 and 45
factoring 3803
3803 is prime (unsat)
factoring 45
factors of 45 are 3 and 15
factoring 3
3 is prime (unsat)
factoring 15
factors of 15 are 5 and 3
factoring 5
5 is prime (unsat)
factoring 3
3 is prime (unsat)
factoring 3607
3607 is prime (unsat)
[2, 3, 3, 5, 3607, 3803]
python z.py  19.30s user 0.02s system 99% cpu 19.443 total

So, 1234567890 = 2*3*3*5*3607*3803.

One important note: there is no primality test, no lookup tables, etc. Prime number is a number for which "x*y=prime" (where x>1 and y>1) diophantine equation (which allows only integers in solution) has no solutions. It can be solved for real numbers, though.

Z3 is not yet good enough for non-linear integer arithmetic and sometimes returns "unknown" instead of "unsat", but, as Leonardo de Moura (one of Z3's author) commented about this:

...Z3 will solve the problem as a real problem. If no real solution is found, we know there is no integer solution.
If a solution is found, Z3 will check if the solution is really assigning integer values to integer variables.
If that is not the case, it will return unknown to indicate it failed to solve the problem.
( https://stackoverflow.com/questions/13898175/how-does-z3-handle-non-linear-integer-arithmetic )

Probably, this is the case: we getting "unknown" in the case when a number cannot be factored, i.e., it's prime.

It's also very slow. Wolfram Mathematica can factor number around 2^80 in a matter of seconds. Still, I've written this for demonstration.

The problem of breaking RSA is a problem of factorization of very large numbers, up to 2^4096. It's currently not possible to do this in practice.

Next part: Integer factorization using SAT solver.


→ [list of blog posts, my twitter/facebook]

Please drop me email about any bug(s) and suggestion(s): dennis(@)yurichev.com.