Z3でコードを最適化する方法は？ （PI_NON_NESTED_ARITH_WEIGHT関連）

Question

私はan optimization problem for a boolean formula

(set-option :PI_NON_NESTED_ARITH_WEIGHT 1000000000) 

(declare-const a0 Int) (assert (= a0 2)) 
(declare-const b0 Int) (assert (= b0 2)) 
(declare-const c0 Int) (assert (= c0 (- 99999))) 
(declare-const d0 Int) (assert (= d0 99999)) 
(declare-const e0 Int) (assert (= e0 49)) 
(declare-const f0 Int) (assert (= f0 49)) 

(declare-const a1 Int) (assert (= a1 3)) 
(declare-const b1 Int) (assert (= b1 3)) 
(declare-const c1 Int) (assert (= c1 (- 99999))) 
(declare-const d1 Int) (assert (= d1 99999)) 
(declare-const e1 Int) (assert (= e1 48)) 
(declare-const f1 Int) (assert (= f1 49)) 

(declare-const c Int) 
(declare-const d Int) 
(declare-const e Int) 
(declare-const f Int) 

(define-fun max ((x Int) (y Int)) Int 
    (ite (>= x y) x y)) 

(define-fun min ((x Int) (y Int)) Int 
    (ite (< x y) x y)) 

(define-fun goal ((c Int) (d Int) (e Int) (f Int)) Int 
    (* (- d c) (- f e))) 

(define-fun sat ((c Int) (d Int) (e Int) (f Int)) Bool 
    (and (and (>= d c) (>= f e)) 
     (forall ((x Int)) (=> (and (<= a0 x) (<= x b0)) 
           (> (max c (+ x e)) (min d (+ x f))))))) 

(assert (and (sat c d e f) 
      (forall ((cp Int) (dp Int) (ep Int) (fp Int)) (=> (sat cp dp ep fp) 
                   (>= (goal c d e f) (goal cp dp ep fp)))))) 

(check-sat) 

を解決することを目的とz3のコードを持っている私はそれが理由数量詞と意味合いの、このコードは、多くの費用がかかるていると思います。私はライン上でそれをテストしたとき、それは私に2回の警告を与え、最終的な結果はunknownです：それは良い結果を得ることから避けるこれらの2回の警告である場合

failed to find a pattern for quantifier (quantifier id: k!33) 
using non nested arith. pattern (quantifier id: k!48), the weight was increased to 1000000000 (this value can be modified using PI_NON_NESTED_ARITH_WEIGHT=<val>). timeout`. 

は、誰も私に教えてもらえますか？このコードを最適化して実行する方法はありますか？

Answer 1

私は以下の反復的な方法で、Z3のいくつかの呼び出しを使用して解決策を検索するループで、Z3の最適化問題を解決しました。

1. あなたのケースで溶液（、(sat c d e f)

2. 計算そのソリューションの価値（あなたのソリューションがc0、d0、e0、f0、ある場合には(goal c0 d0 e0 f0)を評価するための解決策を探す。その呼び出し値v0

3. 新しい問題の解決策を見つける(and (sat c1 d1 e1 f1) (> (goal c1 d1 e1 f1) v0))

4. ポイント3がUNSATを返す場合、v0が最大です。ない場合は、v0として新しいソリューションを使用すると、ポイント3

に戻ってあなたが時々すなわちcu、du、eu、fu(and (sat c d e f) (<= (goal cu du eu fu))があるような値（最初の上限を推測して、プロセスをスピードアップすることができますUNSAT）し、二分法で進める。

私の経験では、繰り返しの方法は最適化の問題のために量子を使うよりはるかに高速です。

Answer 2

SoftTimur：あなたの問題は、整数の上での非線形演算（ゴール関数の中での）を含んでいるため、あなたが遭遇した他の問題を解決することができても、あなたの問題に "不明"非線形整数算術は決めることができないので、Z3の現在のソルバーが量子の存在下で問題を効率的に処理することはほとんどありません。 （もちろん、驚くべきZ3の人々は、この特定の問題に対処するためにソルバーをちょうど "正しい"ものに微調整することができますが、一般的に決定不可能な問題は残ります）。非線形の構造を持たなくても、 SMTソルバーを使用すると、定量化されたアプローチでは遠くに行くことはありません。

フィリップスの本質的なアイデアは、繰り返しを使用することです。しかし、私は、2つの方法（反復対定量）が同等ではないことを強調したいと思います。理論的には、定量化アプローチはより強力です。たとえば、Z3に最大の整数値（単純な最大化問題、ここでコストは整数自体の値）を与えるように頼むと、そのような整数が存在しないことを正しく伝えます。しかし、反復的なアプローチに従えば、永遠にループします。一般に、最適化問題に対する全体的な最大値/最小値が存在しない場合、反復的な方法は失敗する。理想的には、定量化ベースのアプローチではそのようなケースに対処できますが、それはあなた自身が観察したように他の制限があります。

Z3（とSMTソルバー）のように、SMT-Libを使ってプログラミングするのはちょっと難しいことです。だからこそ、多くの人々がより使いやすいインターフェースを構築しています。たとえば、Haskellを使用している場合は、HaskellからZ3をスクリプト化するSBVバインディングを試すことができます。実際、私はあなたの問題をHaskellでコード化しました：http://gist.github.com/1485092。 （あなたのSMTLibコードを誤解している可能性があり、コードミスをしている可能性があることを念頭に置いてください）

HaskellのSBVライブラリでは、定量化アプローチと反復的アプローチの両方を最適化できます。私が量子を使ってz3を試してみると、Z3は実際には "未知"を返します。つまり、問題は決定できません。 （プログラムの "test1"関数を参照してください）反復バージョン（関数 "test2"を参照）を試しても、より良い、より良い解決策が見つかったので、約10分後に次の解を見つけて殺しました：

*** Round 3128 **************************** 
*** Solution: [4,42399,-1,0] 
*** Value : 42395 :: SInteger 

問題のこの特定のインスタンスが実際に最適な解決策を持っているかどうかを知っていますか？そうであれば、プログラムをもっと長く走らせることができ、最終的にはそれを見つけることができます。そうでなければ、永遠に進むでしょう。

あなたがHaskellパスを探索することを選択した場合、それに問題がある場合はお知らせください。