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 ( library(clpb) )。

示例查询使用sat/1：

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

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

要触发所有解决方案的智能暴力枚举，请使用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谓词来解决它，该谓词创建了一个预定义列表，每个变量只有一个元素：

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 回答
-1

我是否理解您，您对单一模型感到满意。您不需要标签或 sat_count。这是一个替代模型查找器，与您的相似，但只会返回一致的模型。

由于它找到反模型，因此您需要提供公式的否定来找到模型。谓词迷宫/3 是作为肯定谓词证明/2 的否定实现而开发的：

% Find a counter model.
% maze(+Norm,+List,-List)
maze(or(A,_),L,_) :- member(A,L), !, fail.
maze(or(A,B),L,R) :- !, inv(A,C), maze(B,[C|L],R).
maze(and(A,_),L,R) :- maze(A,L,R), !.
maze(and(_,B),L,R) :- !, maze(B,L,R).
maze(A,L,_) :- member(A,L), !, fail.
maze(A,L,M) :- oneof(L,B,R), connective(B), !, 
                 inv(A,C), inv(B,D), maze(D,[C|R],M).
maze(A,L,[B|L]) :- inv(A,B).

它可以找到以下所有谬误的反模型：

Affirming a Disjunct: (p v q) & p => ~q.
Affirming the Consequent: (p => q) & q => p.
Commutation of Conditionals: (p => q) => (q => p).
Denying a Conjunct: ~(p & q) & ~p => q.
Denying the Antecedent: (p => q) & ~p => ~q.
Improper Transposition: (p => q) => (~p => ~q).

这是一个示例运行：

Jekejeke Prolog 2, Runtime Library 1.2.5
(c) 1985-2017, XLOG Technologies GmbH, Switzerland

?- negcase(_,N,F), norm(F,G), maze(G,[],L), 
   write(N), write(': '), sort(L,R), write(R), nl, fail; true.
Affirming a Disjunct: [pos(p),pos(q)]
Affirming the Consequent: [neg(p),pos(q)]
Commutation of Conditionals: [neg(p),pos(q)]
Denying a Conjunct: [neg(p),neg(q)]
Denying the Antecedent: [neg(p),pos(q)]
Improper Transposition: [neg(p),pos(q)]

有趣的是，这比 CLP(B) 快得多。以下是在 CLP(B) 和迷宫中运行相同问题的一些时间：

?- time((between(1,1000,_), negcaseclp(_,N,F,L),
   sat(~F), once(labeling(L)), fail; true)).
% Up 296 ms, GC 3 ms, Thread Cpu 250 ms (Current 01/27/18 00:34:20)
Yes 
?- time((between(1,1000,_), negcase(_,_,F),
   norm(F,G), maze(G,[],_), fail; true)).
% Up 82 ms, GC 0 ms, Thread Cpu 78 ms (Current 01/27/18 00:30:21)
Yes
于 2018-01-26T23:12:35.180 回答