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.
→ [list of blog posts]Please drop me email about any bug(s) and suggestion(s): dennis(@)yurichev.com.