3

質問: z3 でモデルの戻り値の設定を制御することはできますか?

例:次の命題論理式を考えると、2 つの可能なモデルがあります。

  • a: True, b: True, c: False (優先)
  • a: True, b: False, c: True (引き続き有効、「第 2 選択」のみ)

aブール式/アサーション自体を介して、モデル whereおよびbare がモデル whereおよびareTrueよりも優先されるように制御したいと思います。ただし、追加の制約が追加されたためにそうできなかった場合は、 withおよびbeingを返す必要があります。acTruebTrueacTrue

SMT2 フォーミュラ: これは、rise4fun でテストできる SMT2 のフォーミュラの例です。

(declare-const a Bool)
(declare-const b Bool)
(declare-const c Bool)

(assert (= a true))
(assert (or
    (and (= b true) (not (= c true)))
    (and (= c true) (not (= b true)))
))

(check-sat)
(get-model)

観察:節内の節の順序を実際に切り替えることによって、返されるモデルに含まれているかどうかを制御することが実際に可能であるように思われることに気付きbました。これは何らかの形で信頼できるものですか、それともこの些細な例で偶然に起こっているだけですか?cTrueandor

4

3 に答える 3

3

これは、assert-softコマンドを使用する別の回答です。

代替エンコーディング #1

最初にOptiMathSATのエンコーディングを提供し、次にこれらの式を変更してz3で同じ結果を得る方法を説明します。他のアプローチと比較して、このエンコーディングは、同じ優先度レベルを共有する多くのブール変数がある場合により適しています。これにより、OMT ソルバーは辞書式検索の各ステップに専用の MaxSAT エンジンを使用するか、カーディナリティ ネットワークを使用してパフォーマンスを向上させることができます。標準の OMT ベースの検索。

次のように、他の回答で示した2つのおもちゃの例を1つの増分式で混同しました。

(set-option :produce-models true)
(set-option :opt.priority lex)

(declare-const a Bool)
(declare-const b Bool)
(declare-const c Bool)

(assert (= a true))
(assert (or
    (and (= b true) (not (= c true)))
    (and (= c true) (not (= b true)))
))

(assert-soft a :weight 1 :id highest_priority)
(assert-soft b :weight 1 :id medium_priority)
(assert-soft c :weight 1 :id lowest_priority)

(minimize highest_priority)
(minimize medium_priority)
(minimize lowest_priority)

; First Solution

(check-sat)
(get-objectives)
(get-model)

; Second Solution

(push 1)
(assert (not (and a b)))

(check-sat)
(get-objectives)
(get-model)
(pop 1)

(exit)

これは出力です：

~$ optimathsat test.smt2 
sat

(objectives
 (highest_priority 0)
 (medium_priority 0)
 (lowest_priority 1)
)
( (a true)
  (b true)
  (c false)
  (highest_priority 0)
  (medium_priority 0)
  (lowest_priority 1) )
sat

(objectives
 (highest_priority 0)
 (medium_priority 1)
 (lowest_priority 0)
)
( (a true)
  (b false)
  (c true)
  (highest_priority 0)
  (medium_priority 1)
  (lowest_priority 0) )

このエンコーディングをz3で使用するには、次の 3 行をコメント アウトするだけで十分です。

;(minimize highest_priority)
;(minimize medium_priority)
;(minimize lowest_priority)

これは、z3がコマンドの目的を暗黙的に定義し、assert-softそれを暗黙的に最小化するためです。その出力は次のとおりです。

~$ z3 test.smt2 
sat
(objectives
 (highest_priority 0)
 (medium_priority 0)
 (lowest_priority 1)
)
(model 
  (define-fun b () Bool
    true)
  (define-fun c () Bool
    false)
  (define-fun a () Bool
    true)
)
sat
(objectives
 (highest_priority 0)
 (medium_priority 1)
 (lowest_priority 0)
)
(model 
  (define-fun b () Bool
    false)
  (define-fun c () Bool
    true)
  (define-fun a () Bool
    true)
)

z3は暗黙的に最小化目標を宣言するため、assert-softコマンドは関連する目的関数に割り当てたい優先順位と同じ順序で表示される必要があることに注意してください。

incipit で述べたように、このエンコーディングは、いくつかの変数が同じレベルの優先度を共有している場合、他の回答のエンコーディングよりもはるかに優れています。2 つの変数a1をa2同じレベルの優先度で配置するにはid、それらのassert-softコマンドに同じものを使用できます。

例えば：

(set-option :produce-models true)
(set-option :opt.priority lex)

(declare-const a1 Bool)
(declare-const a2 Bool)
(declare-const a3 Bool)
(declare-const b1 Bool)
(declare-const b2 Bool)
(declare-const c Bool)

(assert (= a1 true))
(assert (or
    (and (= b1 true) (not (= c true)))
    (and (= c true) (not (= b1 true)))
))

(assert (or (not a1) (not a2) (not a3) ))
(assert (or (not b1) (not b2) ))

(assert-soft a1 :weight 1 :id highest_priority)
(assert-soft a2 :weight 1 :id highest_priority)
(assert-soft a3 :weight 1 :id highest_priority)

(assert-soft b1 :weight 1 :id medium_priority)
(assert-soft b2 :weight 1 :id medium_priority)

(assert-soft c :weight 1 :id lowest_priority)

(minimize highest_priority)
(minimize medium_priority)
(minimize lowest_priority)

; First Solution

(check-sat)
(get-objectives)
(get-model)

; Second Solution

(push 1)
(assert (not (and a1 b1)))

(check-sat)
(get-objectives)
(get-model)
(pop 1)

(exit)

出力で

~$ optimathsat test.smt2 
sat

(objectives
 (highest_priority 1)
 (medium_priority 1)
 (lowest_priority 0)
)
( (a1 true)
  (a2 true)
  (a3 false)
  (b1 false)
  (b2 true)
  (c true)
  (highest_priority 1)
  (medium_priority 1)
  (lowest_priority 0) )
sat

(objectives
 (highest_priority 1)
 (medium_priority 1)
 (lowest_priority 0)
)
( (a1 true)
  (a2 true)
  (a3 false)
  (b1 false)
  (b2 true)
  (c true)
  (highest_priority 1)
  (medium_priority 1)
  (lowest_priority 0) )

代替エンコーディング #2

興味深い事実は、辞書式最適化エンジンなしで辞書式最適化assert-soft問題を解決するために使用できることです。同じ結果を得るには、重みを少し操作するだけで十分です。これは、SAT/MaxSAT 解法の場合に伝統的に行われていることです。唯一の注意点は、ウェイトを慎重に配置する必要があることです。それ以外では、このアプローチは上記のエンコーディングよりもさらに効率的である可能性があります。これは、最適化の問題全体が内部の単一目的エンジンへの単一の呼び出しで解決されるためです。

(set-option :produce-models true)
(set-option :opt.priority lex)

(declare-const a Bool)
(declare-const b Bool)
(declare-const c Bool)

(assert (= a true))
(assert (or
    (and (= b true) (not (= c true)))
    (and (= c true) (not (= b true)))
))

(assert-soft a :weight 4 :id obj) ; highest priority
(assert-soft b :weight 2 :id obj)
(assert-soft c :weight 1 :id obj) ; lowest priority

(minimize obj)

; First Solution

(check-sat)
(get-objectives)
(get-model)

; Second Solution

(push 1)
(assert (not (and a b)))

(check-sat)
(get-objectives)
(get-model)
(pop 1)

(exit)

これは出力です：

~$ optimathsat test.smt2 
sat

(objectives
 (obj 1)
)
( (a true)
  (b true)
  (c false)
  (obj 1) )
sat

(objectives
 (obj 2)
)
( (a true)
  (b false)
  (c true)
  (obj 2) )

他の回答へのコメントでこれについて言及しましたが、別の潜在的に興味深い解決策は、式のビットベクターエンコーディングを試してから、OBVBS ( Nadel et al. による「ビットベクター最適化」を参照) を BVに使用することです。 - 最上位ビットが優先度の最も高い変数を表し、最下位ビットが優先度の最も低い変数を表すベクトルの最適化。

試してみたい場合は、少し前に OptiMathSAT に論文で説明されている OBVBS エンジンの再実装を導入しました。Z3 はビットベクター最適化もサポートしています。

于 2018-11-25T21:14:21.110 に答える
2

a順序, b,が与えられた場合、c考えられるアイデアは、おもちゃの例をOptimization Modulo Theoryでエンコードし、辞書式最適化エンジンを使用することです。

(set-option :produce-models true)
(set-option :opt.priority lex)

(declare-const a Bool)
(declare-const b Bool)
(declare-const c Bool)

(assert (= a true))
(assert (or
    (and (= b true) (not (= c true)))
    (and (= c true) (not (= b true)))
))

(maximize (ite a 1 0)) ; highest priority
(maximize (ite b 1 0))
(maximize (ite c 1 0)) ; lowest priority

(check-sat)
(get-objectives)
(get-model)

同じ構文を受け入れるため、z3またはOptiMathSATのいずれかでこれを解決できます。

~$ optimathsat test.smt2 
sat

(objectives
 ((ite a 1 0) 1)
 ((ite b 1 0) 1)
 ((ite c 1 0) 0)
)
( (a true)
  (b true)
  (c false) )

~$ z3 test.smt2 
sat
(objectives
 ((ite a 1 0) 1)
 ((ite b 1 0) 1)
 ((ite c 1 0) 0)
)
(model 
  (define-fun b () Bool
    true)
  (define-fun c () Bool
    false)
  (define-fun a () Bool
    true)
)

次のように、組み合わせを禁止する制約を追加するとa /\ bします。

(set-option :produce-models true)
(set-option :opt.priority lex)

(declare-const a Bool)
(declare-const b Bool)
(declare-const c Bool)

(assert (= a true))
(assert (or
    (and (= b true) (not (= c true)))
    (and (= c true) (not (= b true)))
))
(assert (not (and a b)))

(maximize (ite a 1 0))
(maximize (ite b 1 0))
(maximize (ite c 1 0))

(check-sat)
(get-objectives)
(get-model)

次に、ソルバーは他の解を見つけます。

~$ optimathsat test.smt2 
sat

(objectives
 ((ite a 1 0) 1)
 ((ite b 1 0) 0)
 ((ite c 1 0) 1)
)
( (a true)
  (b false)
  (c true) )

~$ z3 test.smt2 
sat
(objectives
 ((ite a 1 0) 1)
 ((ite b 1 0) 0)
 ((ite c 1 0) 1)
)
(model 
  (define-fun b () Bool
    false)
  (define-fun c () Bool
    true)
  (define-fun a () Bool
    true)
)

注 1.私は可能な限り単純な方法で目標をコード化しましたが、これが目的の目標を達成するための最良の方法であるとは限らないことに注意してください。問題に含まれる変数の数と問題自体の構造に応じて、他の可能なエンコーディングを検討する必要があります(たとえば、目的関数に別の定式化を使用する、いくつかの変数に対する分岐優先度を設定するなどの API のみの機能を使用する、エンコードするビットベクトルの問題) . また、SMT 固有の機能が必要でない限り、辞書式最適化機能を備えた SAT/MaxSAT ソルバーを探すことをお勧めします。

注2.モデルに対する好みの概念が、おもちゃの例から推測した「辞書編集の好み」よりも一般的である場合でも、ニーズにより適した代替コスト関数定義で最適化モジュロ理論を使用できます。

注 3. (コメントから) 2 つの変数a1とa2が同じ優先度レベルを共有する必要がある場合、それらは同じminimize/maximizeディレクティブに配置する必要があります(maximize (+ (ite a1 1 0) (ite a2 1 0)))。

于 2018-11-25T20:11:29.663 に答える