prolog - bool 公式的蛮力 Prolog SAT 求解器

Question

我正在尝试编写一个算法来天真地寻找 bool 公式(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

使用clpb !

:- use_module (library(clpb))。

使用 sat/1 的示例查询:

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

一些变量( A 和 B )已经精确地绑定(bind)到一个 bool 值(在上面的查询中)，但搜索尚未完成(由剩余目标指示)。

要触发所有解决方案的智能暴力枚举，请使用 labeling/1 像这样:

?- sat(~(~ (A * B) + (C * D))), labeling ([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。