1

ブール式の最適化問題z3を解決することを目的としたコードがあります

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

量指定子と含意のためだと思いますが、このコードには多くのコストがかかります。オンラインでテストしたところ、2 つの警告が表示され、最終結果はunknown次のようになりました。

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`.

良い結果が得られないのがこれらの2つの警告であるかどうか、誰か教えてもらえますか? このコードを最適化して実行する方法はありますか?

4

2 に答える 2

3

SoftTimur：問題には整数に対する非線形演算（ゴール関数内）が含まれるため、発生した他の問題を解決できたとしても、Z3は問題に「不明」と応答する可能性があります。非線形整数演算は決定不能であり、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パスを探索することを選択した場合、および問題がある場合はお知らせください。

于 2011-12-16T08:47:19.193 に答える
3

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

  1. 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は、最大です。そうでない場合は、新しいソリューションを as として使用し、v0ポイント 3 に戻ります。

最初に上限 (つまりcu、UNSATなどの値) を推測しdu、次に二分法で処理を進めることでeu、プロセスを高速化できる場合があります。fu(and (sat c d e f) (<= (goal cu du eu fu))

私の経験では、最適化問題で量指定子を使用するよりも反復的な方法の方がはるかに高速です。

于 2011-12-15T18:53:10.240 に答える