5

ブール式 (NNF、CNF ではない) のモデルを単純に検索するアルゴリズムを作成しようとしています。

私が持っているコードは既存のモデルをチェックできますが、モデルを見つけるように求められたときに失敗します (または終了しません) member(X, Y)。[X|_], [_,X|_], [_,_,X|_]...

私がこれまでに持っているのはこれです：

:- op(100, fy, ~).    
:- op(200, xfx, /\).  
:- op(200, xfx, \/).  
:- op(300, xfx, =>).  
:- op(300, xfx, <=>). 

formula(X) :- atom(X).
formula(~X) :- formula(X).
formula(X /\ Y) :- formula(X), formula(Y).
formula(X \/ Y) :- formula(X), formula(Y).
formula(X => Y) :- formula(X), formula(Y).
formula(X <=> Y) :- formula(X), formula(Y).

model(1, _).
model(X, F) :- atom(X), member([X, 1], F).
model(~X, F) :- atom(X), member([X, 0], F). % NNF
model(A /\ B, F) :- model(A, F), model(B, F).
model(A \/ B, F) :- (model(A, F); model(B, F)).
model(A => B, F) :- model(~A \/ B, F).
model(A <=> B, F) :- model((A => B) /\ (B => A), F).

sat(A) :- model(A, F), \+ (member([X, 1], F), member([X, 0], F)).


%%% examples:
% formula(~(~ (a /\ b) \/ (c => d))).
% model(a, [[a,1]]).

のより良いデータ構造F、または部分的にインスタンス化されたリストを切り捨てることができる他の方法はありますか?

編集: 定義と例を追加しました。

4

3 に答える 3

3

を使用してください！

:- use_module (ライブラリ(clpb) )。

を使用したサンプル クエリsat/1:

?- sat (~(~ (A * B) + (C * D)))。
A = B、B = 1、sat(1#C*D)。

一部の変数 (AおよびB)は、(上記のクエリで) 正確に 1 つのブール値に既にバインドされていますが、検索はまだ完了していません (これは、残りの目標によって示されます)。

すべてのソリューションのスマートな総当たり列挙をトリガーするには、次のlabeling/1ように使用します。

?- sat(~(~ (A * B) + (C * D)))、ラベリング([A,B,C,D])。
   A = B、B = 1、C = D、D = 0
; A = B、B = D、D = 1、C = 0
; A = B、B = C、C = 1、D = 0。
于 2015-12-18T09:02:22.737 に答える
1

generate_model各変数に対して正確に1つの要素を持つ事前定義されたリストを作成する述語を書くことでそれを解決しました:

generate_model([], []).
generate_model([X|T], [[X,_]|T2]) :- generate_model(T, T2).

sat(A) :- 
  var_list(A, Vars),
  generate_model(Vars, F),
  model(A, F).
于 2015-12-17T19:16:07.413 に答える