簡化表達式會導致超時

Question

如何使用Z3求解器簡化下列表達式？

(declare-const c0 Int) 
(declare-const c1 Int) 
(declare-const c2 Int) 

(assert (let ((a!1 (to_real (+ (* (* 2 c0) c2) 
        (* (* 2 c0) c1) 
        (* 2 c1 c2) 
        (* c0 (- c0 1)) 
        (* c1 (- c1 1)))))) 
    (let ((a!2 (/ (to_real (* (* 2 c0) c2)) a!1))) 
    (and (or (and (<= c2 1) (>= c2 1) (<= c0 2) (>= c0 2) (<= c1 3) (>= c1 3)) 
      (and (<= c2 1) (>= c2 1) (<= c0 3) (>= c0 3) (<= c1 2) (>= c1 2))) 
    (= (/ 2.0 15.0) a!2)))) 
) 

(apply (then qe propagate-values (repeat (then ctx-solver-simplify propagate-ineqs) 10))) 

鏈接：http://rise4fun.com/Z3/u7F7

我嘗試了所有可能的戰術，我知道，但最終通過求解導致超時。有什麼方法可以避免超時？是否因爲在Java API中返回false？

Answer 1

僅僅通過查看代碼很難說出發生了什麼。但我認爲to_real可能是有問題的部分，因爲域之間的轉換傾向於生成非線性約束，這可能會導致複雜性問題。

我給它用純粹雷亞爾一試（即宣告c0，c1 ..如Real秒;以及刪除呼叫to_real）

如果你確實需要的整數/實數混合;確保在葉子處進行混合（即在常數下）;或在最頂端，儘可能多地推動轉換;而不是中間值。

但是我猜想如果你的問題空間允許的話，那麼堅持到雷爾斯將是這裏的方式。

Answer 2

該示例使用非線性整數算術。不幸的是，在Z3不終止的這個域中很容易產生例子。 ctx-solver-simplify例程多次調用SMT求解程序，並且在每個調用中都必須檢查某些非線性約束組合的可滿足性。