有等式Pell 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)
Run Code Online (Sandbox Code Playgroud)
结果: [y = 2744248620923429728, x = 8169167793018974721]
为什么?
PS有效答案:[y = 448036604040,x = 6224323426849]