布尔公式的蛮力 Prolog SAT 求解器答案

【问题标题】：Brute-force Prolog SAT solver for boolean formulas布尔公式的蛮力 Prolog SAT 求解器
【发布时间】：2015-12-17 19:06:35
【问题描述】：

我正在尝试编写一个算法来天真地寻找布尔公式（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 是否有更好的数据结构，或者其他方式可以截断部分实例化的列表？

编辑：添加定义和示例。

【问题讨论】：

请将您的代码自成一体，以便其他人实际尝试。
抱歉，我在其余代码中进行了编辑。
关于表示的一条评论：您知道每个这样的列表正好有 2 个元素。在这种情况下，最好使用x=0、x=1 之类的术语来更紧凑地表示绑定：[x,0] 是 .(x, .(0, [])，浪费空间用于一个额外的仿函数 ./2 和一个原子 []这样的结构。相比之下，x=0 是 =(x,0)，即只有一个函子及其两个参数。正如其他人所说，您实际上可以通过使用实际的逻辑变量轻松地将绑定委托给 Prolog。您可以存储符号/变量对应而不是变量/值一！

标签： prolog sat clpb

【解决方案1】：

使用clpb！

:- use_module(library(clpb))。

使用sat/1的示例查询：

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

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

要触发所有解决方案的智能暴力枚举，请使用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。

【讨论】：

【解决方案2】：

我通过编写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).

【讨论】：

我觉得generate_model/2 很像term_variables/2，我是不是遗漏了什么？
@DanielLyons。我同意。确实如此。 term_variables/2 加上一些合适的 maplist/3... 直接使用逻辑变量会更惯用（而且很可能更快）。此外，它可以防止使用F 像[[x,0],[x,1],...] （这很糟糕！）
哦，太棒了！尽管在这种特定情况下，公式本身并不包含真正的 Prolog 变量——每个“变量”都由一个原子术语（通常是一个字符串）表示。然后我的var_list 谓词列出唯一原子，就像term_variables 列出变量一样。
是的，我想在这种情况下逻辑变量会更好——但我们所做的大部分工作是符号操作而不是评估。我需要它来自动检查 equisatisfiability 以验证某些 Tseytin 实现的正确性。
如果您的语义与 Prolog 足够相似，您可以让它为您完成提升。 :)

【解决方案3】：

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

由于它找到反模型，您需要提供公式的否定来找到模型。谓词迷宫/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

【讨论】：