4

因此？

我的问题发生的用例上下文

我定义了一个三角形的 3 个随机项。Microsoft Z3 应输出：

  • 约束是否满足或是否有无效的输入值？
  • 所有其他三角形项目的模型，其中所有变量都分配给具体值。

为了约束我需要assert三角形等式的项目 - 我想从勾股定理（(h_c² + p² = b²) ^ (h_c² + q² = a²)）开始。

问题

我知道 Microsoft Z3 解决非线性算术问题的能力有限。但即使是一些手动计算器也能够解决这样一个非常简化的版本：

(set-option :print-success true)
(set-option :produce-proofs true)
(declare-const a Real)
(declare-const b Real)
(assert (= a 1.0))
(assert (= b 1.0))
(assert
    (exists
        ((c Real))
        (=
            (+
                (* a a)
                (* b b)
            )
            (* c c)
        )
    )
)
(check-sat)
(get-model)

问题

  • 如果给出两个值，有没有办法让 Microsoft Z3 解决勾股定理？
  • 或者：是否有另一个定理证明器能够处理这些非线性算术的情况？

感谢您对此的帮助 - 如果有任何不清楚的地方，请发表评论。

4

1 回答 1

4

Z3 有一个用于非线性算术的新求解器 (nlsat)。它比其他求解器更有效（请参阅本文）。新的求解器对于无量词问题是完整的。但是，新的求解器不支持生成证明。如果我们禁用证明生成，那么 Z3 将使用 nlsat 并轻松解决问题。根据您的问题，您似乎真的在寻找解决方案，因此禁用证明生成似乎不是问题。

此外，Z3 不会产生近似解（如手算器）。它使用实数代数的精确表示。我们还可以要求 Z3 以十进制表示法显示结果（选项:pp-decimal）。 这是您的在线示例。

在此示例中，当使用精确表示时，Z3 将显示以下结果c。

(root-obj (+ (^ x 2) (- 2)) 1)

据说这是c多项式的第一个根x^2 - 2。当我们使用(set-option :pp-decimal true)时，它会显示

(- 1.4142135623?)

问号用于表示结果被截断。请注意，结果是否定的。但是，它确实是您发布的问题的解决方案。由于您正在寻找三角形，因此您应该断言常量都 > 0。

顺便说一句，您不需要存在量词。我们可以简单地使用一个常量c。这是一个示例（也可以在rise4fun 在线获得）：

(set-option :pp-decimal true)
(declare-const a Real)
(declare-const b Real)
(declare-const c Real)
(assert (= a 1.0))
(assert (= b 1.0))
(assert (> c 0))
(assert (= (+ (* a a) (* b b)) (* c c)))
(check-sat)
(get-model)

这是另一个没有解决方案的示例（也可以在rise4fun 在线获得）：

(set-option :pp-decimal true)
(declare-const a Real)
(declare-const b Real)
(declare-const c Real)
(assert (> c 0))
(assert (> a c))
(assert (= (+ (* a a) (* b b)) (* c c)))
(check-sat)

顺便说一句，您应该考虑Z3 的 Python 接口。它对用户更加友好。我链接的教程在运动学中有示例。他们还使用非线性算术来编码简单的高中物理问题。

于 2013-02-27T14:35:54.210 回答