z3 - Need help understanding the equation

Question

Have the equation Pell x*x - 193 * y*y = 1

in z3py:

x = BitVec('x',64)
y = BitVec('y',64)
solve(x*x - 193 * y*y == 1, x > 0, y > 0)

Result: [y = 2744248620923429728, x = 8169167793018974721]

Why?

P.S. Valid answer: [y = 448036604040, x = 6224323426849]

Answer 1

It is possible to use Bit-vector arithmetic to solve Diophantine equations. The basic idea is to use ZeroExt to avoid the overflows pointed out by Pad. For example, if we are multiplying two bit-vectors x and y of size n, then we must add n zero bits to x and y to make sure that the result will not overflow. That is, we write:

 ZeroExt(n, x) * ZeroExt(n, y)

The following set of Python functions can be used to "safely" encode any Diophantine equation D(x_1, ..., x_n) = 0 into Bit-vector arithmetic. By "safely", I mean if there is a solution that fits in the number of bits used to encode x_1, ..., x_n, then it will eventually be found modulo resources such as memory and time. Using these function, we can encode the Pell's equation x^2 - d*y^2 == 1 as eq(mul(x, x), add(val(1), mul(val(d), mul(y, y)))). The function pell(d,n) tries to find values for x and y using n bits.

The following link contains the complete example: http://rise4fun.com/Z3Py/Pehp

That being said, it is super expensive to solve Pell's equation using Bit-vector arithmetic. The problem is that multiplication is really hard for the bit-vector solver. The complexity of the encoding used by Z3 is quadratic on n. On my machine, I only managed to solve Pell's equations that have small solutions. Examples: d = 982, d = 980, d = 1000, d = 1001. In all cases, I used a n smaller than 24. I think there is no hope for equations with very big minimal positive solutions such as d = 991 where we need approximately 100 bits to encode the values of x and y. For these cases, I think a specialized solver will perform much better.

BTW, the rise4fun website has a small timeout, since it is a shared resource used to run all research prototypes in the Rise group. So, to solve non trivial Pell's equations, we need to run Z3 on our own machines.

def mul(x, y):
  sz1 = x.sort().size()
  sz2 = y.sort().size()
  return ZeroExt(sz2, x) * ZeroExt(sz1, y)
def add(x, y):
  sz1 = x.sort().size()
  sz2 = y.sort().size()
  rsz = max(sz1, sz2) + 1
  return ZeroExt(rsz - sz1, x) + ZeroExt(rsz - sz2, y)  
def eq(x, y):
  sz1 = x.sort().size()
  sz2 = y.sort().size()
  rsz = max(sz1, sz2)
  return ZeroExt(rsz - sz1, x) == ZeroExt(rsz - sz2, y)
def num_bits(n):
  assert(n >= 0)
  r = 0
  while n > 0:
    r = r + 1
    n = n / 2
  if r == 0:
    return 1
  return r
def val(x):
  return BitVecVal(x, num_bits(x))
def pell(d, n):
  x  = BitVec('x', n)
  y  = BitVec('y', n)
  solve(eq(mul(x,x), add(val(1), mul(val(d), mul(y, y)))) , x > 0, y > 0)