Hilbert’s 10th problem, Fermat’s last theorem and SMT solvers

Hilbert's 10th problem states that you cannot devise an algorithm which can solve any diophantine equation over integers. However, it's important to understand, that this is possible over fixed-size bitvectors.

Fermat's last theorem states that there are no integer solution(s) for $a^n + b^n = c^n$, for $n>=3$.

Let's prove it for n=3 and for a in 0..255 range:

from z3 import *

# for a 8-bit bitvec, to prevent overflow during multiplication/addition, 25 bits must be allocated
# because log2(256)*3 = 8*3 = 24
# and a sum of two 24-bit bitvectors can be 25-bit
a,b,c = BitVecs ('a b c', 25)

s=Solver()

# only 8-bit values are allowed in these 3 bitvectors:
s.add((a&0xfffff00)==0)
s.add((b&0xfffff00)==0)
s.add((c&0xfffff00)==0)

# non-zero values:
s.add(a!=0)
s.add(b!=0)
s.add(c!=0)

# a^3 + b^3 = c^3
s.add(a*a*a + b*b*b == c*c*c)

print s.check()


Z3 gives "unsat", meaning, it couldn't find any a/b/c. However, this is possible to check even using brute-force search.

If to replace "BitVecs" by "Ints", Z3 would give "unknown":

from z3 import *

a,b,c = Ints ('a b c')

s=Solver()

s.add(a!=0)
s.add(b!=0)
s.add(c!=0)

# a^3 + b^3 = c^3
s.add(a*a*a + b*b*b == c*c*c)

print s.check()


In short: anything is decidable (you can build an algorithm which can solve equation or not) under fixed-size bitvectors. Given enough computational power, you can solve such equations for big bit-vectors. But this is not possible for integers or bit-vectors of any size.

Another interesting reading about this by Leonardo de Moura: https://stackoverflow.com/questions/13898175/how-does-z3-handle-non-linear-integer-arithmetic.

→ [back to the main page]