1

我的例子：方程组

伪代码约束库 
  a = b+c
∧ e = a*c

∧ a = +2     ; some replaceable concrete values
∧ c = +18
解决方案 
  b = -16
∧ e = -32

我想要的信息

在方程组中，我想获得以下知识：

我可以用来从给定值（在约束基础中）计算变量值（解决方案）的抽象公式。

（就像在高中，老师不仅想要看到结果，还想要这样一个转换的抽象公式。）

像...这样的公式 
  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`

我的问题

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

谢谢。- 如果有任何不清楚的地方，请评论什么是错的。

4

1 回答 1

5

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

你描述的问题很有趣，但也不是微不足道的。一般来说，输入不仅仅是一组方程。此外，即使我们只有方程，但它们是非线性的，那么可能无法获得像您的问题中描述的那样的“已解决”形式。在非线性情况下，我们可以将方程组以三角形形式表示，但仅此而已。另一个问题是，即使解的数量是有限的，它也不像线性情况那样是唯一的。此外，一般来说，非线性方程组的解不能用根式表示。在内部，Z3 使用实数代数来表示解决方案。

于 2013-03-01T03:21:36.920 回答