2

命題充足可能性 (量化子を使用) と線形演算を含む問題を解決しようとしています。

私は問題を定式化し、Z3 はそれを解決できますが、不当に長い時間がかかります。

戦術を特定してZ3を助けようとしてきましたが、あまり進歩していません（論理理論の知識はありません）。

以下は、私が解決しようとしているものの本質を捉えた非常に単純化された問題です。誰でも提案できますか？

ネルソン・オッペン法などを読んでみましたが、見慣れない表記が多く、習得に時間がかかりそうです。

また、Z3 ではユーザーがこれらの構成を微調整できますか? 最後に、これらの戦術を z3py で使用するにはどうすればよいですか?

(declare-datatypes () ((newtype (item1) (item2) (item3))))

(declare-fun f (newtype newtype) Bool)

(declare-fun cost (newtype newtype) Real)

(assert (exists ((x newtype)(y newtype)) (f x y)))

(assert (forall ((x newtype)(y newtype)) (=> (f x y) (> (cost x y) 0))))

(assert (forall ((x newtype) (y newtype)) (<= (cost x y) 5)))

(check-sat)

(get-model)
4

1 に答える 1

1

エンコードしたサンプル問題は、数量化を使用しています。Z3 は、モデルベースの数量化子のインスタンス化 (mbqi オプション) と呼ばれる、数量化された式のクラスの充足可能性を決定する特定の手順を使用します。これは、数式の量指定子のない部分の候補モデルを、量指定子のモデルにも拡張することによって機能します。このプロセスには、多くの検索が含まれる場合があります。オプション /st を指定して Z3 を実行することにより、検索プロセスから統計を抽出できます。検索プロセスの選択された統計が表示され、検索中に何が起こっているかを大まかに把握できます。算術演算と量指定子を持つ式のクラスに特化した特定の戦術の組み合わせはありません (そのような式のデフォルトの戦術によって処理されるビットベクトルと量指定子を使用する式のクラスがあります)。

ネルソン・オッペン法などを読んでみましたが、見慣れない表記が多く、習得に時間がかかりそうです。

これは、量指定子を使用した検索の問題を理解するのに少し関係があります。

また、Z3 ではユーザーがこれらの構成を微調整できますか?

はい、コマンドラインから Z3 を設定できます。たとえば、コマンド ラインを使用して MBQI を無効にすることができます。

z3 tt.smt2 -st smt.auto_config=false smt.mbqi=false

Z3 は「unknown」を返すようになりました。これは、選択されたインスタンス化を実行する弱い量指定子エンジンでは、式が満足できるかどうかを判断できないためです。コマンド ライン オプションについては、「z3 -?」の指示に従って学習できます。

最後に、これらの戦術を z3py で使用するにはどうすればよいですか?

z3py のタクティクスを使用できます。ファイル z3.py には、戦術を組み合わせる方法の簡単な情報が含まれています。ただし、問題クラスの難しさは、量指定子に関連する検索の難しさに実際に関係していると思います。これらの式のクラスは一般に非常に決定不可能であるため、定理証明が発散する量化子を使用して式を提示することは非常に簡単です。

于 2013-12-12T17:28:37.400 に答える