Z3Py：从方程组生成抽象公式 [英] Z3Py: Generating Abstract Formulas From A System Of Equations

问题描述

我的示例：方程组

伪代码约束基础 b

  a = b + c 
∧e = a * c 
 
∧a = +2;一些可替换的具体值
∧c = +18 
  

  b = -16 
∧e = -32 
  

我想要的信息

在方程组中，我想得到以下知识： / p>

抽象公式可用于从给定值计算变量值约束基础）。

（像在高中，老师不只是想看结果，而是这样一个变换的抽象公式。）

公式喜欢...

  b = ac ;是从a = b + c'
∧e =（a-c）* c的等价变换;是一个术语替换`b→ac'的`e = a * c` 
  

h2>

如何使用 Z3Py 从Z3约束系统方程中检索此信息？

谢谢。

解决方案

Z3不是提取这类信息的理想工具。
在内部，它有可能有用的模块（例如，高斯消除， Groebner Basis ）用于在特定情况下实现此类功能，但它们不会在Z3 API中公开。
Z3源代码可在线获取。

问题描述是有趣的，但它也是不平凡的。一般来说，输入不仅仅是一组方程。此外，即使我们只有方程，但它们是非线性的，那么它可能不可能得到一个解决形式，如你的问题中描述的形式。在非线性情况下，我们可以将方程式以三角形形式，但是它是。另一个问题是，即使解的数量是有限的，它不是唯一的，在线性情况下。
此外，一般来说，非线性方程组的解不能使用自由基来表示。在内部，Z3使用真实代数数字用于表示解。

My Example: system of equations

Pseudo-Code Constraint Base

  a = b+c
∧ e = a*c

∧ a = +2     ; some replaceable concrete values
∧ c = +18

Solution

  b = -16
∧ e = -32

The Information I Want

In a system of equations, I want to get the following knowledge:

Abstract formulas which I can use to compute the variable values (the solution) from the given values (in the constraint base).

(Like in high school where the teacher don't just wanted the see the result, but also such an transformated abstract formula.)

Formulas Like ...

  b = a-c     ; is an equivalent transformation from `a = b+c`
∧ e = (a-c)*c ; is an term replacement `b → a-c` of `e = a*c`

My Question

How can I use Z3Py retrieve this information from a Z3 constraint system of equations?

Thanks. - If anything's unclear, please comment concerning what's wrong.

解决方案

Z3 is not the ideal tool for extracting this kind of information. Internally, it has modules (e.g., Gaussian elimination, Groebner Basis) that may be useful for implementing this kind of functionality for particular cases, but they are not exposed in the Z3 API. The Z3 source code is available online.

The problem you described is interesting, but it is also non trivial. In general, the input is not just a set of equations. Moreover, even if we have only equations, but they are nonlinear, then it may not be possible to get a "solved" form like the one described in your question. In the nonlinear case, we may put the equations in triangular form, but that is it. Another issue is that even when the number of solutions is finite, it is not unique like in the linear case. Moreover, in general, the solution of a nonlinear set of equations can't be expressed using radicals. Internally, Z3 uses real algebraic numbers for representing the solution.

这篇关于Z3Py：从方程组生成抽象公式的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！