問題タブ [dpll]

合成可能な Verilog ですべてのデジタル フェーズ ロックを実装する簡単な方法はありますか? すべて (VCO を含む) を合成する必要があります。ロックしようとしている信号は、システム クロック周波数の約 0.1 ～ 1% です。1980 年代の IEEE 論文から再構築したものを使用していますが、宣伝されているほど動作しません。

簡単にするために、ロックはバイナリパルス信号で動作します。

C++ でDPLLアルゴリズムを実装しようとしていますが、このタイプの再帰問題を解決するにはどのようなデータ構造が最適か疑問に思っています。現在、ベクターを使用していますが、コードが長くて見にくいです。何か提案はありますか？

最近、私はHaskellにナイーブなDPLL Sat Solverを実装しました。これは、JohnHarrisonのHandbookof Practical Logic andAutomatedReasoningを基にしています。

DPLLはさまざまなバックトラック検索であるため、 Oleg KiselyovetalのLogicモナドを使用して実験したいと思います。しかし、何を変える必要があるのか​​よくわかりません。

これが私が持っているコードです。

• ロジックモナドを使用するには、どのコードを変更する必要がありますか？
• ボーナス：ロジックモナドを使用することによる具体的なパフォーマンス上の利点はありますか？

ウィキペディアで説明されているように、C++でDPLLアルゴリズムを実装しています。

しかし、ひどいパフォーマンスをしています。このステップでは：

現在、私はのコピーを作成することを避けようとしてΦいますが、代わりに、lまたはnot(l)の唯一のコピーを追加して、/if 'sが戻っΦたときにそれらを削除します。これはアルゴリズムを壊して間違った結果を与えるようです（セットがであるとしても）。DPLL()falseUNSATISFIABLESATISFIABLE

このステップで明示的なコピーを回避する方法に関する提案はありますか？

ここに私のメイクファイルがあります

そして私のOCamlファイルはこのようなものです(そのdpll部分)。

次のエラーが発生しました。

では、どうすればそれをリンクできますか？

どうもありがとう

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

私は Haskell の全くの初心者で、DPLL を使用して単純な SAT ソルバーを作成しようとしています。

(A1 and A2 ...) Or (B1 and B2 ...)スキーマを結合正規形にする関数 expand があります: (A1 or B1) and (A1 or B2) and ... (A2 or B2) and ...。

式のデータ型を次のように表しました

(-x で Not(x) を表すことができるので、否定は気にしません)

しかし今、expand を書いていると、これはコンストラクタータグで非常に見苦しくなります。

このコードをよりきれいにすることはできますか?

プロファイラー gprof を使用して (疑似非線形) 整数実数フラグメント (呼び出しグラフを含む統計) にある問題をプロファイリングし、2 つのクラスにかかった時間を分離しようとしました。

I) SAT 解決部分 ([純粋に] ブール伝搬と [純粋に] ブール競合節の検出、バックジャンプ、その他の命題操作を含む)

II) 理論解決部分 (理論の一貫性チェック、理論の矛盾節の生成、理論の伝播を含む)。

smt_context.cpp の3280 ～ 3346行目bounded_search()はトップレベルの DPLL(X) ループを構成していますか?

SATソルバー関数の時間を合計する方が簡単だと思います（数が少ないため）。残りは理論ソルバーの時間と見なすことができます。上記のクラス I に該当すると見なすべき関数を見つけようとしています。彼らsmt::context::decide()は、smt::context::bcp()内にいますsmt::context::propagate()か？他のもの？ smt::context: resolve_conflict()理論ソルバーへの呼び出しと混在しているようですか?

smt::context::propagate()機能以外はほとんど理論伝播（クラスII）のように見えるのは正しいbcp()ですか？また、smt::context::final_check()純粋にクラス II にあるようです。

どんなヒントでも大歓迎です。ありがとう。

Z3 の算術ソルバーは、DPLL(T) とシンプレックス (この論文で説明) に基づいて開発されています。また、競合の説明が生成されたときに Z3 がバックトラックを実行する方法がわかりません。例を挙げます：

線形算術式は次のとおりです。

(2x1+x2≤200 OR 3x1+x2≤250) AND (2x1+x2+x3≤200 OR 4x1+2x2+x3≤400) AND x1≥50 AND x2≥50 AND x3≥60

2x1+x2≤200、2x1+x2+x3≤200、x1≥50、x2≥50および連続してアサートした後x3≥60、競合説明セット が生成され{2x1+x2+x3≤200, x1≥50, x2≥50, x3≥60}ます。

私の質問は、この競合セットが生成されたときにバックトラックがどのように実行されるかです。