問題タブ [clpb]

シンプルな Prolog SAT ソルバーを構築しようとしています。私の考えでは、ユーザーは Prolog リストを使用して CNF (Conjucutive Normal Form) で解くブール式を入力する必要があります。たとえば、(A または B) および (B または C) は sat([[A, B] 、[B、C]]) であり、Prolog は A、B、C の値を見つけます。

次のコードが機能せず、その理由がわかりません。トレース呼び出しのこの行: (7) sat([[true, true]]) ? start_solve_clause([_G609, _G612]]) を期待していました。

免責事項:数日前の Prolog や SAT の問題についても知らなかったくだらないコードで申し訳ありません。

PS: SAT の解決に関するアドバイスは大歓迎です。

痕跡

プロローグソース

Prolog を学習しながら、CNF 問題 (パフォーマンスは問題ではありません) を解決するプログラムを作成しようとしたため、次のコードを解決することになりました(!x||y||!z)&&(x||!y||z)&&(x||y||z)&&(!x||!y||z)。

この宣言型言語を使用して CNF を解決する、より簡単で直接的な方法はありますか?

私はプロローグの制約処理の問題を解決しようとしています。

5x5、4x4、3x3、2x2の4つの正方形を10x10のグリッドに詰める必要があります。それらは重複してはいけません。

私の変数は次のようになります。

Xは5、4、3または2のいずれかです。インデックスiは行を表し、ドメインはグリッド内の列を表します。

私の最初の制約は、正方形の幅と高さを定義しようとします。私はそれをそのように定式化します：

そのため、可能なポイントは、互いにX行と列の範囲内に収まるように制限されます。ただし、Prologはこれらの制約で停止し、次の結果をもたらします。

したがって、他の正方形をチェックすることさえせずに、そこで停止します。私の制約はおそらくきつすぎるでしょうが、その理由や方法がわかりません。助言がありますか？

プロローグで次の述語を実装し、真理値表に使用したい: and/2、or/2、nand/2、nor/2、xor/2

たとえば and/2 を実装する方法を誰かが教えてくれるので、自分で他の実装を行ってここに投稿できます。

これまでのところ、このプログラムは GNU プロローグで動作するようになりました

and(p,q) と入力して yes を取得することも、and(p,not(q)) を入力して no を取得することもできます。今、私はこのようなことをしたいと思います:

p を true に設定し (p.) で初期化し、(and(p,q)) を true に設定し (ただし、q を初期化せずに)、プロローグに次のように言ってもらいたい: 1 つの解決策が存在する: "q" は true でなければならない)

p と (or(p,q)) を true に設定すると、プロローグに次のように言わせます。それを行う最良の方法はどれですか？

次のキャリバンの問題を解き、各手がかりを「忠実に」プロローグに変換します。つまり、可能な限り忠実に変換します。

抽象化の簡単な演習として、4 つの無意味な記号 a、b、c、および d が、同じ順序で無意味な記号 w、x、y、および z に対応すると仮定し、さらに次のように仮定します。

a が x でない場合、c は y ではありません。
b が y または z の場合、a は x です。
c が w でない場合、b は z です。
d が y の場合、b は x ではありません。
d が x でない場合、b は x です。

2 組の記号が対応する順序は?

次のコードを試しました：

しかし、それはfail.Anyヘルプをいただければ幸いです。

次の形式のデータがあります。

図: https://docs.google.com/drawings/d/10wBpmFxxbDqrlpPVqpkVo_r8I-qcalWAz7Lro9myjMs/edit?usp=sharing

デバイスへの入力も AND ゲートに似ていますが、常に回路ツリーの「最上位」レベルにあります。次のような結果になる述語を実装したいと思います。

そしてもちろん、 のはるかに単純な構造ですd2。

これにより、clpb ライブラリを使用して、入力のインスタンス化を行って、どのデバイスがオンまたはオフになっているかを知ることも、デバイスをオンにするためにオンにする必要がある入力を見つけることもできます。

しかし、何度も試みたにもかかわらず、これらの構造を正しく構築することができませんでした。

V 変数にこのように名前を付ける必要はありませんが、sat ステートメントの変数が正しい入力変数と一致することが重要です。

私はプロローグの初心者であり、再帰的に考えるのが難しいと感じています。list1[0,0,0,1,1,0,1,1]、list2[1,0,1,0,0,0,1,1] という 2 つのリストがあるとします。また、list1 または list 2 の対応する位置に 1 がある場合、1 を持つリストを返したいと考えています。

上記のフォームでのたうち回ることができないことはわかっていますが、これは今のところプロローグのフォームに近いものです。再帰はとても難しいようです！