布尔公式的暴力Prolog SAT求解器

Question

我正在尝试编写一种天真寻找布尔公式(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,或者某些其他方式可以切断部分实例化的列表？

编辑:添加了定义和示例.

Answer 1

我通过编写一个generate_model谓词来解决这个问题，该谓词创建了一个预定义列表，其中每个变量只有一个元素：

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).