Z3 の実行からいくつかの統計を取得しました。これらが何を意味するのかを理解する必要があります。私はかなり錆びていて、sat と SMT 解決の最近の開発については最新ではありません。このため、私は自分で説明を見つけようとしましたが、完全に間違っている可能性があります。したがって、私の質問は主に次のとおりです。
1) メジャーの名前は何を意味しますか?
2) 間違っている場合は、彼らが何を指しているのかをよりよく理解するための指針を教えてもらえますか?
その他の所見は以下で行われ、概念的には上記の 2 つの質問に属します。前もって感謝します！
私の解釈は次のとおりです。
DPLL。以下のすべてのメトリックは、ほとんどのソルバーの基礎である DPLL アルゴリズムの専門用語を参照しています。
- :決定事項
- 決定の数
- :伝播
- 伝播数（ユニット伝播だと思います）
- :2進伝播、 : 3進伝播
- 一度に 2 つまたは 3 つのリテラルの伝播
- :競合
- 競合の数
- :決定事項
解決策。大まかに言えば、句をセットとして解釈する操作が行われました。SATを解決するためのもう1つのパラダイムである解決から得られたテクニック。
- :包含
- :仮定の解決
- 上記の2つの違いは何ですか？
- :dyn-subsumption-resolution
- ここで説明する必要があります: Hamadi et al. による動的な包摂のための学習。
その他のテクニック
- :minimized-lits
- 明確なアイデアはありません。それはおそらく節学習に関連していますか？
- :probing-assigned
- 「プロービング」時に行われた割り当ての数をカウントしていると思いますが、これはある種の先読み手法だと思います。
- :del節
- 削除された節の数 (理由は何ですか? 冗長ですか?)
- : elim-literals : elim-clauses : elim-bool-vars : elim-blocked-clauses
- elim-が削除された後のエンティティの数。これらのメトリクスは、特定の SAT 解決手法を参照します (参照については、M.Järvisalo らによるブロックされた句の削除を参照してください)。
- :再起動
- 再起動の数。
- :minimized-lits
その他の側面
- :mk-bool-var : mk-binary-clause : mk-ternary-clause : mk-clause
- ブール変数と、作成された 2 項、3 項、およびジェネリック句の数。
- ：メモリー
- 使用されるメモリの最大量。
- :gc 句
- ガベージコレクション節…？
- 私の実験によると、この解釈はもっともらしいです。
- : gc-clause <= : del-clause ; 私の場合、不等式は厳密です。
- 常にそうであるとは限りません
- : gc-clause <=: elim-clauses ; 次のようにすることもできます: gc-clause > : elim-clauses
- :mk-bool-var : mk-binary-clause : mk-ternary-clause : mk-clause