z3處理非線性實數算法的侷限性

Question

我有一個程序在非線性實數算術中產生一組約束。考慮以下兩個約束：

（<（ - （ - （ - （+（*（ - 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）（ - （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_x v3_x））（*（ - v2_y v3_y）（ - v2_y v3_y）））） （*（ - v2_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） （*（ - v_y v2_y） （*（ - v0_y v2_y）（*（ - v3_x v2_y）（ - v3_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_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是否有可能處理上述限制（比如通過改變其制定方式或其他方式）？

Answer 1

是的，當我們將(< ... 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使用的算法描述爲here。該算法使用基於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))