3

我有一个程序可以在非线性实数算术中生成一组约束。考虑以下两个约束：

(<(- (- (- (+ (* (- v0_x v3_x) (- v1_y v3_y) (+ (* (- v2_x v3_x) (- v2_x v3_x))) (* (- v2_y v3_y) (- v2_y v3_y)))) (* (- v0_y v3_y) (- v2_x v3_x) (+ (* (- v1_x v3_x) (- v1_x v3_x)) (* (- v1_y v3_y) (- v1_y v3_y)))) (* (- v1_x v3_x) ( - v2_y v3_y) (+ (* (- v0_x v3_x) (- v0_x v3_x)) (* (- v0_y v3_y) (- v0_y v3_y))))) (* (- v1_y v3_y) (- v2_x v3_x) (+ ( * (- v0_x v3_x) (- v0_x v3_x)) (* (- v0_y v3_y) (- v0_y v3_y))))) (* (- v0_y v3_y) (- v1_x v3_x) (+ (* (- v2_x v3_x) ( - v2_x v3_x)) (* (- v2_y v3_y) (- v2_y v3_y))))) (* (- v0_x v3_x) (- v2_y v3_y)(+ (* (- v1_x v3_x) (- v1_x v3_x)) (* (- v1_y v3_y) (- v1_y v3_y))))) 0)

(>(- (- (- (+ (* (- v0_x v2_x) (- v1_y v2_y) (+ (* (- v3_x v2_x) (- v3_x v2_x))) (* (- v3_y v2_y) (- v3_y v2_y)))) (* (- v0_y v2_y) (- v3_x v2_x) (+ (* (- v1_x v2_x) (- v1_x v2_x)) (* (- v1_y v2_y) (- v1_y v2_y)))) (* (- v1_x v2_x) ( - v3_y v2_y) (+ (* (- v0_x v2_x) (- v0_x v2_x)) (* (- v0_y v2_y) (- v0_y v2_y))))) (* (- v1_y v2_y) (- v3_x v2_x) (+ ( * (- v0_x v2_x) (- v0_x v2_x)) (* (- v0_y v2_y) (- v0_y v2_y))))) (* (- v0_y v2_y) (- v1_x v2_x) (+ (* (- v3_x v2_x) ( - v3_x v2_x)) (* (- v3_y v2_y) (- v3_y v2_y))))) (* (- v0_x v2_x) (- v3_y v2_y)(+ (* (- v1_x v2_x) (- v1_x v2_x)) (* (- v1_y v2_y) (- v1_y v2_y))))) 0)

当我将它们断言给 Z3 时，它说它是可满足的，但是一旦我将第二个约束更改为 (< ... 0) 而不是 (> ... 0) 现在应该是不可满足的，z3 就会永远运行。我想知道 z3 在处理非线性实数算术方面的局限性。Z3 是否有可能处理上述约束（例如通过更改它们的制定方式或任何其他方式）？

4

1 回答 1

4

是的，当我们改变问题时，问题变得(< ... 0)无法(> ... 0)满足，并且有一个简单的证明，因为它变成了p < 0 and p > 0. 简化后，您帖子中的两个多项式是相同的。然而，Z3 错过了这个简单的证明。这将在下一个版本中修复。同时，我们可以通过使用自定义策略来捕获具有这种简单证明的示例。

(check-sat-using (then (! simplify :som true) (! simplify :sort-sums true) smt))

该策略执行多项式归一化并调用一个引擎来检测 和 中的p < 0不一致性p > 0。整个示例可在线获取：http ://rise4fun.com/Z3/JP4 。我也把它贴在了邮件的最后。

Z3 一直在运行，因为它错过了简短/简单的证明，并尝试使用更昂贵和更完整的方法找到证明。Z3 使用的算法在此处描述。该算法使用基于子结果的投影算子。此操作非常昂贵，并且会为您的示例生成非常大的多项式。此过程适用于包含小型多项式的问题，其中每个多项式都有一小组变量。未来，我们计划结合完整和不完整的技术，改进 Z3 可以在合理时间内解决的问题集。

(declare-const v0_x Real)
(declare-const v1_x Real)
(declare-const v2_x Real)
(declare-const v3_x Real)
(declare-const v4_x Real)
(declare-const v0_y Real)
(declare-const v1_y Real)
(declare-const v2_y Real)
(declare-const v3_y Real)
(declare-const v4_y Real)


(assert
(< (- (- (- (+ (* (- v0_x v3_x) (- v1_y v3_y) (+ (* (- v2_x v3_x) (- v2_x v3_x)) (* (- v2_y v3_y) (- v2_y v3_y)))) (* (- v0_y v3_y) (- v2_x v3_x) (+ (* (- v1_x v3_x) (- v1_x v3_x)) (* (- v1_y v3_y) (- v1_y v3_y)))) (* (- v1_x v3_x) (- v2_y v3_y) (+ (* (- v0_x v3_x) (- v0_x v3_x)) (* (- v0_y v3_y) (- v0_y v3_y))))) (* (- v1_y v3_y) (- v2_x v3_x) (+ (* (- v0_x v3_x) (- v0_x v3_x)) (* (- v0_y v3_y) (- v0_y v3_y))))) (* (- v0_y v3_y) (- v1_x v3_x) (+ (* (- v2_x v3_x) (- v2_x v3_x)) (* (- v2_y v3_y) (- v2_y v3_y))))) (* (- v0_x v3_x) (- v2_y v3_y) (+ (* (- v1_x v3_x) (- v1_x v3_x)) (* (- v1_y v3_y) (- v1_y v3_y))))) 0.0))

(assert
(< (- (- (- (+ (* (- v0_x v2_x) (- v1_y v2_y) (+ (* (- v3_x v2_x) (- v3_x v2_x)) (* (- v3_y v2_y) (- v3_y v2_y)))) (* (- v0_y v2_y) (- v3_x v2_x) (+ (* (- v1_x v2_x) (- v1_x v2_x)) (* (- v1_y v2_y) (- v1_y v2_y)))) (* (- v1_x v2_x) (- v3_y v2_y) (+ (* (- v0_x v2_x) (- v0_x v2_x)) (* (- v0_y v2_y) (- v0_y v2_y))))) (* (- v1_y v2_y) (- v3_x v2_x) (+ (* (- v0_x v2_x) (- v0_x v2_x)) (* (- v0_y v2_y) (- v0_y v2_y))))) (* (- v0_y v2_y) (- v1_x v2_x) (+ (* (- v3_x v2_x) (- v3_x v2_x)) (* (- v3_y v2_y) (- v3_y v2_y))))) (* (- v0_x v2_x) (- v3_y v2_y) (+ (* (- v1_x v2_x) (- v1_x v2_x)) (* (- v1_y v2_y) (- v1_y v2_y))))) 0.0))

(check-sat-using (then (! simplify :som true) (! simplify :sort-sums true) smt))
于 2012-12-04T21:48:35.057 回答