z3 处理非线性实数算法的局限性 [英] z3 limitations in handling nonlinear real arithmetics

问题描述

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

I have a program that generates a set of constraints in nonlinear real arithmetic. Consider the following two constraints:

(< (- (- (- (- (+ (* (- 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 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)

(> (- (- (- (+ (* (- 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 有没有可能处理上述约束(比如通过改变它们的制定方式或任何其他方式)?

when I assert them to Z3, it says that it is satisfiable, but as soon as I change the second constraint to (< ... 0) instead of (> ... 0) which should be now unsatisfiable, z3 runs forever. I am wondering about the limitations of z3 for handing nonlinear real arithmetic. Is there any chance that Z3 can handle the above constraints (like by changing the way they are formulated or any other way)?

推荐答案

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

Yes, when we change (< ... 0) to (> ... 0) the problem becomes unsatisfiable, and there is a trivial proof for that since it becomes p < 0 and p > 0. The two polynomials in your post are identical after simplifications. However, Z3 misses this simple proof. This is be fixed in the next releases. In the meantime, we can catch examples that have this kind of simple proof by using a custom strategy.

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

此策略进行多项式归一化并调用检测p <中不一致的引擎.0 和 p >0.整个示例可在以下网址获得:http://rise4fun.com/Z3/JP4.我也贴在了留言的最后.

This strategy does the polynomial normalization and calls an engine that detects the inconsistency in p < 0 and p > 0. The whole example is available online at: http://rise4fun.com/Z3/JP4. I also pasted it in the end of the message.

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

Z3 keeps running forever because it misses the short/easy proof and tries to find the proof using more expensive and complete methods. The algorithm used by Z3 is described here. The algorithm uses a projection operator based on subresultants. This operation is very expensive, and produces very big polynomials for your example. This procedure works well for problems containing small polynomials with a small set of variables on each of them. In the future, we plan to combine complete and incomplete techniques and improve the set of problems that Z3 can solve in a reasonable amount of time.

(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))

这篇关于z3 处理非线性实数算法的局限性的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！