問題タブ [sat-solvers]

図に示すようなメッシュ ネットワークがあります。現在、この sat ネットワークのすべてのエッジに値を割り当てています。プログラムで、割り当てに閉じたループがないことを提案したいと思います。たとえば、左上の四角形の制約は次のように記述できます -

E0 = 0 or E3 = 0 or E4 = 0 or E7 = 0であるため、ループを形成しないようにするには、どちらかのリンクを非アクティブにする必要があります。ただし、この種のネットワークでは、多くのループが発生する可能性があります。

たとえば、エッジによって形成されるループ - E0, E3, E7, E11, E15, E12, E5, E1。

ここでの問題は、このネットワークで発生する可能性のあるループの可能な組み合わせをそれぞれ説明する必要があることです。1つの可能な式で制約を書き込もうとしましたが、うまくいきませんでした。

この状況をエンコードする方法があれば、誰でもポインタを投げることができますか? 参考までに、私は Z3 Sat Solver を使用しています。

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 らによるブロックされた句の削除を参照してください)。
  • :再起動
    • 再起動の数。

• その他の側面

  • :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

リンク:
Z3 定理証明者
picosat と pyhton バインディング

Z3 を SAT ソルバーとして使用しました。より大きな数式ではパフォーマンスの問題があるように思われるため、ピコサットをチェックして、それがより高速な代替手段であるかどうかを確認したかったのです. 私の既存の python コードは、z3 構文で命題式を生成します。

出力/結果

ただし、Picosat は、次の例に示すように、数値のリスト/配列を使用します (「clauses1」: 6 は変数 P を参照し、-6 は「非 P」を意味するなど)。

CNF の式を表す Z3 変数 (コード例の変数 "f" など) を、picosat が CNF の式を表すために使用する前述の形式に変換するための簡単なソリューションとして何をお勧めしますか? Z3 の python API を実際に使用してみましたが、ドキュメントが不十分で、自分で問題を解決することはできませんでした。

(上記の例は単に概念を示しているだけであることに注意してください。変数 C で表される式は動的に生成され、z3 で直接効率的に処理するには複雑すぎます)

簡単な問題。mxn マトリックスを表す非常に大きな CNF ファイルがあります。関連する用語を含む >10000 変数としましょう。したがって、最初のステップとして、CNF ファイルを分割するか、並列解決の概念のために行列を 100 の変数に分割することをお勧めします。どのルールを適用するかについての説明はありますか?

すべての助けに感謝します。

エイドリアンよろしく

SMT でモデル化したい 2 つの句があるとしましょう。

または、このようなand演算子を使用して1つのアサーションを追加します

これは、SMT ソルバーのパフォーマンスに関して大規模な問題に関係しますか。Z3を使用しています。

次の行に沿って、定義されたタイムアウト期間内に終了する必要がある子プロセスを開始しています。

子プロセスは、CPU 集中型の計算エンジン (SAT ソルバー) です。私のメイン プログラムは、Visual Studio 2013とWindows 7 64 ビットC#を使用して記述および開発されています。

ほとんどの場合、上記のコードは機能し、適切なプロセス タイムアウト終了が達成されます。しかし、ケースの約 5%process.Kill()では、目に見える効果はありません。子プロセスはアクティブなままです。

優先度の低い子プロセスを開始しようとしました。また、殺す前に一時停止しようとしました。外部ツールとして呼び出すTASKKILL /Fことも、常に役立つとは限りませんでした。すべての SAT ソルバーで問題が発生するわけではないことに気付きました。管理者権限はありますが、メイン プログラムを管理者として実行していません。

アプリケーションの子プロセスを確実に終了するにはどうすればよいですか?

編集:
タイムアウト バジェットを超えることは別として、子プロセスは非常に正常に動作し、Process Explorer を使用して (管理者の昇格なしで) 手動で強制終了できます。問題は、タイムアウト後にプロセスが実行されていないことを確認する方法です。

回避策: VC++ 2013
を使用してタイムアウト ツールを実装しました。子プロセスを直接呼び出すのではなく、子プロセスを呼び出すツールを呼び出すようになりました。このツールは、CreateProcess()とTerminateProcess()を使用して、子プロセスを開始および停止しています。追加のプロセスを生成せずに、 CreateProcess()およびTerminateProcess()をプログラムから直接呼び出すことはおそらく可能です。 回避策はエレガントではありませんが、私の問題は解決します。C#