Нужна помощь в понимании уравнения

Question

Уравнение Пелла x*x - 193 * y*y = 1

в z3py:

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

Результат: [y = 2744248620923429728, x = 8169167793018974721]

Зачем?

PS Допустимый ответ: [y = 448036604040, x = 6224323426849]

Answer 1

Возможно использовать бит-векторную арифметику для решения диофантовых уравнений. Основная идея заключается в использовании ZeroExt чтобы избежать переливов, указанных Pad. Например, если мы умножаем два битовых вектора x а также y размера nтогда мы должны добавить n ноль битов x а также y чтобы убедиться, что результат не будет переполнен. То есть мы пишем:

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

Следующий набор функций Python может использоваться для "безопасного" кодирования любого диофантова уравнения D(x_1, ..., x_n) = 0 в бит-векторную арифметику. Под "безопасным" я подразумеваю, если есть решение, которое соответствует количеству битов, используемых для кодирования x_1,..., x_n, то в конечном итоге он будет найден по модулю ресурсов, таких как память и время. Используя эти функции, мы можем закодировать уравнение Пелла x^2 - d*y^2 == 1 как eq(mul(x, x), add(val(1), mul(val(d), mul(y, y)))), Функция pell(d,n) пытается найти значения для x а также y с помощью n биты.

Следующая ссылка содержит полный пример: http://rise4fun.com/Z3Py/Pehp

При этом решить уравнение Пелла с помощью арифметики битовых векторов очень дорого. Проблема в том, что умножение действительно трудно для решателя битовых векторов. Сложность кодирования, используемого Z3, является квадратичной по n, На моей машине мне удалось решить только уравнения Пелла, которые имеют небольшие решения. Примеры: d = 982, d = 980, d = 1000, d = 1001, Во всех случаях я использовал n меньше чем 24, Я думаю, что нет надежды на уравнения с очень большими минимальными положительными решениями, такими как d = 991 где нам нужно примерно 100 бит для кодирования значений x а также y, Я думаю, что для этих случаев специализированный решатель будет работать намного лучше.

Кстати, у сайта rise4fun небольшой тайм-аут, поскольку он является общим ресурсом, используемым для запуска всех исследовательских прототипов в группе Rise. Итак, чтобы решить нетривиальные уравнения Пелла, нам нужно запустить Z3 на наших собственных машинах.

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)