問題タブ [dpll]

私は SAT ソルバー (主に DPLL または部分 DPLL) を行っており、Unit Propogation の方法があります。基本的には、スタンドアロンのリテラルがあるかどうかをチェックし、そのリテラルと、他の句で見つかったインスタンスを削除します。任意の例は

ユニットの伝播は「x」になり、ユニットのプロップを実行すると、(w,z)

このメソッドには、いくつかのネストされたforeachループがあり、2 つの変数(bool) と charList<literals> <literals>を持つカスタムメイドのクラスです。hasNegationliteralCharacter

コーディングは以下にあり、以下から説明します

私は2つList <literals>ありtemplist、listOfLiterals後者は「親」です

listOfLiteralsその一致のエントリを削除しようとしていますがtempList、c2.listOfLiterals.RemoveAll(tempList);デリゲートではないため、明らかにエラーを出力します。

stackoverflow でさえ、私はたくさん検索しましたが、それらのすべてが ID または整数のいずれかと比較されます。私の場合、 2Listsを比較しているだけなので、listOfLiterals と tempList の両方で同じエントリが listOfLiterals から削除されるようにデリゲートを行うにはどうすればよいですか?

どうもありがとう

編集：

リテラル クラス

Prolog で DCG を使用して論理式を解析したいと考えています。

論理項はリストとして表されます。たとえば['x','&&','y']、x ∧ y結果は解析ツリーになりますand(X,Y)(以前と未割り当ての Prolog 変数です)。XY

私はそれを実装し、すべてが期待どおりに機能しますが、問題が 1 つあります。変数を
解析して実際の Prolog 変数を取得する方法と、後で真理値を割り当てる方法がわかりません。'x''y'XY

次のルールのバリエーションを試しました。

• v(X) --> [X].:
  これはもちろん機能しません。返されるだけand('x','y')です。
  しかし、この項の論理変数を一様に Prolog 変数に置き換えることはできますか? 私は述語（同様の問題term_to_atomの解決策として提案されている）を知っていますが、ここでそれを使用して目的の結果を達成できるとは思いません。

• v(Y) --> [X], {nonvar(Y)}.:
  これはバインドされていない変数を返しますが、もちろん、論理変数 ('x'、'y'、...) が既に用語に含まれている場合でも、毎回新しい変数が返さ れるため、目的の結果ではない値['X','&&','X']に評価されます。 and(X,Y).

この問題に対する洗練された、または慣用的な解決策はありますか?

よろしくお願いします！

編集：

この質問の背景は、Prolog でDPLL アルゴリズムを実装しようとしているということです。Prolog バックトラッキング機能を簡単に利用できるように、論理項を Prolog-term に直接解析するのは賢明だと思いました。

• 入力: T = などの論理項[x,'&&',y]
• 解析後の用語: [G_123,'&&',G_456](「実際の」Prolog 変数が含まれるようになりました)
• { boolean(t), boolean(f) } からの値を T の最初のバインドされていない変数に代入します。
• 用語を簡略化します。
• v...割り当てが見つかるまで繰り返すか、v(T) = tまたは検索スペースが枯渇するまでバックトラックします。

私は Prolog にかなり慣れていないので、正直なところ、より良いアプローチを見つけることができませんでした。私はより良い代替案に非常に興味があります！(だから私はこれが私が望んでいるものであることに少し自信があります;-)そしてこれまでのあなたのサポートにとても感謝しています...)

上記の DPLL アルゴリズムを Haskell で実装したいと思います。しかし問題は、複数の if ステートメントを実行する方法がわからないことです。だから私は考えていた、最初の 2 つの if ステートメントのパターン マッチを行うことができます。でも、3回目と4回目はできないの？それらの両方を実行する必要があり、return ステートメントも実行する必要があるためです。

Haskell で上記のような複数の if ステートメントを作成するにはどうすればよいですか? また、私は Haskell にまったく慣れていないので、「複雑な」ことは何もできません。

整数の線形演算とブール変数に対するいくつかのアサーションと、実際の非線形演算とブール変数に対するいくつかのアサーションを持つ SMT 式を作成したいと思います。整数と実数に対するアサーションは、ブール変数のみを共有します。例として、次の式を考えてみましょう。

この式を z3 に入力すると、すぐに「不明」と報告されます。しかし、その整数部分を削除すると、すぐに解が得られます。これは、変数 "r" の制約を満たします。これは、非線形制約自体がソルバーにとって難しくないことを意味していると思います。この問題は、整数に対する (線形) 制約と実数に対する (非線形) 制約の混在にあるはずです。

だから私の質問は次のとおりです。z3 を使用してこの種の混合数式を処理する正しい方法は何ですか (存在する場合)? DPLL(T) についての私の理解では、さまざまな制約に対してさまざまな理論ソルバーを使用して、そのような式を処理できるはずです。私が間違っている場合は、私を修正してください。

現在のブランチで解決策が見つからない場合にアルゴリズムがバックトレースする Z3 の c++ ファイルを見つけようとしています。私はすべてのファイルを調べて、Python ファイルでデバッグ モードを試しましたが、今のところうまくいきません。メソッドに print ステートメントを追加したいだけなので、前のノードに戻って新しいパスを試行するタイミングがわかります。

ありがとう！

実際にコーディングする前に、DPLL手順を理解しようとしています。

たとえば、次の句があります。

ここで、決定変数を d = 0、b = 0 とします。節は次のようになります。

ここで、ユニットの伝播と純粋なリテラル規則がどのように役割を果たすのでしょうか?

また、C3 : {1, !a}- を とるa = 1と、これは になり{1, 0}ます。この句の最終的な値は何ですか? {1} にする必要がありますか?

そして、決定変数を適用した後、いずれかの節に value {!b}、つまりリテラルの否定がある場合、どのように処理を進めればよいでしょうか?