## Explanation of the Greatest Common Divisor using Z3 SMT solver, etc

What is Greatest common divisor (GCD)?

Let's suppose, you want to cut a rectangle by squares. What is maximal square could be?

For a 14*8 rectangle, this is 2*2 square:

**************
**************
**************
**************
**************
**************
**************
**************


->

** ** ** ** ** ** **
** ** ** ** ** ** **

** ** ** ** ** ** **
** ** ** ** ** ** **

** ** ** ** ** ** **
** ** ** ** ** ** **

** ** ** ** ** ** **
** ** ** ** ** ** **


What for 14*7 rectangle? It's 7*7 square:

**************
**************
**************
**************
**************
**************
**************


->

******* *******
******* *******
******* *******
******* *******
******* *******
******* *******
******* *******


14*9 rectangle? 1, i.e., smallest possible.

**************
**************
**************
**************
**************
**************
**************
**************
**************
**************


To compute GCD, one of the oldest algorithms is used: Euclidean algorithm. But, I can demonstrate how to make things much less efficient, but more spectacular.

To find GCD of 14 and 8, we are going to solve this system of equations:

x*GCD=14
y*GCD=8


Then we drop x and y, we don't need them. This system can be solved using paper and pencil, but GCD must be as big as possible. Here we can use Z3 in MaxSMT mode:

#!/usr/bin/env python

from z3 import *

opt = Optimize()

x,y,GCD=Ints('x y GCD')

h=opt.maximize(GCD)

print (opt.check())
print (opt.model())


That works:

sat
[y = 4, x = 7, GCD = 2]


What if we need to find GCD for 3 numbers? Maybe we are going to fill a space with biggest possible cubes?

#!/usr/bin/env python

from z3 import *

opt = Optimize()

x,y,z,GCD=Ints('x y z GCD')

h=opt.maximize(GCD)

print (opt.check())
print (opt.model())


This is 3:

sat
[z = 300, y = 111, x = 100, GCD = 3]


### Couple of words about GCD

GCD of coprimes is 1.

GCD is also a common set of factors of several numbers. This we can see in Mathematica:

In[]:= FactorInteger[300]
Out[]= {{2, 2}, {3, 1}, {5, 2}}

In[]:= FactorInteger[333]
Out[]= {{3, 2}, {37, 1}}

In[]:= GCD[300, 333]
Out[]= 3


I.e., 300=2^2 * 3 * 5^2 and 333=3^2 * 37 and GCD=3, which is smallest factor.

Or:

In[]:= FactorInteger[11*13*17]
Out[]= {{11, 1}, {13, 1}, {17, 1}}

In[]:= FactorInteger[7*11*13*17]
Out[]= {{7, 1}, {11, 1}, {13, 1}, {17, 1}}

In[]:= GCD[11*13*17, 7*11*13*17]
Out[]= 2431

In[]:= 11*13*17
Out[]= 2431


(Common factors are 11, 13 and 17, so GCD = 11*13*17 = 2431.)