数学方程 [关闭]答案

【问题标题】：Mathematic equation [closed]数学方程 [关闭]
【发布时间】：2020-08-18 00:14:16
【问题描述】：

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

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

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

【问题讨论】：

This guide 解释了如何为 Z3Py 初始化变量。

标签： numpy z3py mathematical-expressions

【解决方案1】：

以下是使用 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]

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

【讨论】：

谢谢你的回答，我想再问你一件事，我现在的主要问题是如何只比较这个“ Val * X * X * X - Val * 的前64位X * X + Val * X - Val " 与 S ?
S/X/Val 都被声明为 64 位量，因此它们正好是 64 位。我不确定你所说的“64 个第一位”是什么意思，这就是他们所拥有的。

【解决方案2】：

本文改编自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])
>>>

【讨论】：

忘了第二部分和最后一部分是否定的。只需更改为：coeff = [valA, -valB, valC, -valD]

【解决方案3】：

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

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

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

z3=val/int64 (z3 到单位 val(x-val) 除法单位为初始 val3-²

【讨论】：