数学方程式

Question

我有这个等式：S = val.X^3 - val.X^2 + val.X -val

知道变量都是int64，S和val都是已知值，

解决它的最佳方法是什么，我使用了 numpy 和 Z3，但无法得到正确的答案，任何线索都会有所帮助

Answer 1

改编自https://docs.scipy.org/doc/numpy-1.13.0/reference/generated/numpy.roots.html

>>> import numpy as np
>>> valA=2.1
>>> valC=4.3
>>> valD=5.4
>>> valB=3.2
>>> coeff = [valA, valB, valC, valD]
>>> np.roots(coeff)
array([-1.38548682+0.j        , -0.06916135+1.36058497j,
   -0.06916135-1.36058497j])
>>>

Answer 2

以下是如何使用 z3py 对此进行编码，出于本示例的目的，我将 S 设为 40，将 Val 设为 2，但是您可以在 s.add:

的相应行下方轻松修改这些值

from z3 import *

S   = BitVec ('S', 64)
X   = BitVec ('X', 64)
Val = BitVec ('Val', 64)

s = Solver()
s.add (S == 40)
s.add (Val == 2)
s.add (S == Val * X * X * X - Val * X * X + Val * X - Val)

res = s.check()

if res == sat:
   print s.model()
elif res == unsat:
   print "No solution"
else:
   print "Solver returned: " + res

当我运行它时，我得到：

$ python b.py
[X = 4611686018427387907, Val = 2, S = 40]

这可能看起来令人惊讶，但请记住位向量运算是模块化的；如果您进行计算，您会发现它确实满足您的等式。

Answer 3

s=val.x^3.x^2 + val.x - val

int64 和 s.val 是已知值 z3 是 numphy 单位。

s¹=val/3.到单位 x 将 xΔ2 初始值除以 x-val-¹ 将计算适当添加到 numpy 单元

z3=val/int64 (z3 到单位 val(x-val) 划分单元作为初始 val3-²

数学方程式

Mathematic equation

numpy

mathematical-expressions

z3py