1

(これは私の 2 回目のヘルプの試みです。質問/アプローチが意味をなさない、または明確でない場合は、私に知らせてください。 Z3 と私の SBA)

UFBV Z3 ロジックを使用したリレーショナル仕様の境界検証に取り組んでいます。私が調査している現在の問題は、すべての可能なモデルの改ざんを必要とし (到達可能性述語の否定的な使用のため)、高い境界でのソルバーのパフォーマンスを殺します。

可能性のあるモデルの一部だけが実際に興味深い (他と同形ではない) ため、対称性を破る手法 (SAT 分野で知られている) を導入しようとしています。

ただし、私が対称性破りの公理と呼んでいるものを使用すると、場合によっては Z3 のパフォーマンスを向上させることができますが、ソルバーの一般的な動作は不安定になります。

私のアプローチの 1 つ (最も有望なアプローチだと思います) は、ドメイン間の関係の対称性を破ることに基づいています。これは、関係 R の各ドメイン D と各原子 a \in D 公理を導入し、R^{M} と R^{M[a+1/a]} のバイナリ表現に順序を強制します。ここで、M は仕様のモデル。同種の関係の場合、公理は緩和されます。

R \subset AxA を関係とする。R に対する私のリラックスした対称性の破れの公理は次のようになります。

;; SBA(R, A)_upToDiag
(assert
 (forall ( (ai A) (aj A) )
  (=>
   (bvult ai aj)
   (=>
    (forall ((x A))
     (=>
       (bvult x aj)
       (= (R ai x) (R (bvadd ai (_ bv1 n)) x)) 
     )
    )
    (=>
     (R ai aj)
     (R (bvadd  ai  (_ bv1 n)) aj)
)))))    

;; SBA(R, A)_diag
(assert
 (forall ( (ai A) )
  (=>
   (forall ((x A))
    (=>
      (bvult x ai)
      (= (R ai x) (R (bvadd ai (_ bv1 n)) x)) 
    )
   )
   (=>
    (R ai ai)
    (R (bvadd  ai  (_ bv1 n)) (bvadd  ai  (_ bv1 n)))
))))

私の問題は、この SBA を使用した効果が安定していない/一貫していないことです。バインドとバインド、フォーム仕様とは異なります。また、SBA のすべてまたは 1 つだけを使用すると、パフォーマンスに影響します。

SAT のコンテキストでは、いわゆる対称性破りの述語 (SBP) アプローチの成功は、SAT ソルバーのバックトラッキング機能に基づいています。とりわけ、SBP。

  • Z3 のコンテキストでの相違点 (ある場合) は何ですか?
  • これらの公理を使用して探索空間を剪定するように解決を強制するにはどうすればよいですか (バックトラックする場合)。
  • SBA に (量指定子) パターンを使用すると役立ちますか?

よろしく、

アブバクル アクラフ エル ガジ

4

1 に答える 1

4

Z3 3.2には、数量化された数式を処理するための2つの主要なエンジンがあります。EマッチングとMBQI（モデルベースの数量化子のインスタンス化）です。Eマッチングは、満足できない数式でのみ有効です。Z3は、このエンジンを使用して数式が充足可能であることを示すことができません。MBQIはより高価ですが、いくつかのクラスの数式（数量詞を含む）が充足可能であることを示すことができます。Z3ガイドでは、これら2つのエンジン（およびその他のオプション）について説明しています。重要な問題でZ3を効果的に使用するには、これら2つのエンジンがどのように機能するかを理解することが非常に役立ちます。

対称性の破れは通常、検索スペースを減らすための非常に効果的な方法です。問題で何が起こっているのかを正確に特定することは困難です。不安定な動作について、次の説明が表示されます。

  • MBQIは、SBAを満たすモデルを作成するのに苦労しています。SBAは検索スペースを整理しますが、問題が満たされる場合、Z3はそれらを満たす解釈（モデル）を構築しようとします。したがって、この場合、SBAは単なるオーバーヘッドです。これは、入力式が非常に簡単に満たされる場合に特に当てはまりますが、SBAを追加すると難しくなります。オプションを使用して、この仮説を確認できますMBQI_TRACE=true。Z3は、次のようなメッセージを表示します[mbqi] failed k!18。k![line-number]数量詞IDはどこにありますか。タグを使用して独自のIDを割り当てることができます:qid。次に例を示します。

    （assert（forall（（x T）（y T））（！（=>（and（subtype xy）（subtype yx））（= xy））：qid反対称）））

ところで、を使用してMBQIモジュールを無効にすることができますMBQI=false。

Z3の将来のバージョンでは、一部の定量化された数式に対してMBQIを無効にするオプションを追加する予定です。この機能はSBAに役立つ場合があります。

  • もう1つの説明は、EマッチングがSBAのインスタンスを作成しすぎていることです。オプションを使用して確認できますQI_PROFILE=true。Z3は次のような情報をダンプします：

[quantifier_instances]反対称：12：1：2.00

最初の数は、生成されたインスタンスの数です。それが問題の原因である場合、1つの解決策は、生成するインスタンスが多すぎるSBAに制限パターンを割り当てることです。たとえば、Z3はの(R ai aj)パターンとして使用しSBA(R, A)_upToDiagます。この種のパターンは、2次数のインスタンスを作成する可能性があります。もう1つの実験は、Eマッチングを無効にすることです。例、オプション

AUTO_CONFIG=false EMATCHING=false MBQI=true

上記の構成で関連性の伝播を無効にすることもできます。オプション：RELEVANCY=0。

最後に、別のオプションは、有用であると思われるSBAのインスタンスを生成し、定量化された式を削除することです。

于 2012-02-17T15:23:01.323 に答える