如何在 Python 中使用 Z3 找到拉格朗日插值多项式？

Question

我正在使用 Z3 库和 Python 语言学习数学，但我不知道如何找到基于拉格朗日插值多项式的多项式？ 例如，

I have
f(0) = y0
f(1) = y1
f(2) = y2
....

我想找到 f(X)

我可以很好地使用 Scipy，但是当更改为 Z3 库时，我找不到更多文档了 :(

Answer 1

我不知道如何在 Z3 的上下文中回答您的问题。 Z3 不包含任何用于拉格朗日插值的内置求解器。 您可以设置多项式等式系统，其中系数保持符号化。 然后您可以询问 Z3 系统是否可解。它通常为系数生成代数数，因此我不确定这是否适合您的应用。 当然，在python中你可以这样写：

a, b, c = Real('a b c')
def f(X):
    return a*X*X + b*X + c

solve(f(0) == y0, f(1) == y1, f(2) == y2)

其中y0、y1、y2 是常量。