我有一个生成一组非线性真实算术约束的程序。 考虑以下两个约束：
（<（ - （ - （ - （+（*（ - 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可以（通过改变它们配制的方式或任何其他方式等）处理上述限制？
是的，当我们改变(< ... 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使用的算法描述这里 。 该算法采用基于投影算subresultants 。 此操作是非常昂贵的，并为您的示例产生非常大的多项式。 这个过程非常适用于含有小多项式对他们每个人的一小部分的变量问题。 在未来，我们计划结合起来完全和不完全的技术和完善的一套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))
