如何在 Prolog 中将命题公式转换为析取范式（DNF）？答案

【问题标题】：How to convert a propositional formula to disjunctive normal form (DNF) in Prolog?如何在 Prolog 中将命题公式转换为析取范式（DNF）？
【发布时间】：2013-12-28 10:32:32
【问题描述】：

我是 Prolog 的新手，我需要将结果从真值表转换为析取范式。我已经能够生成给定的真值表：

?- table(p or(q and not r) or not s or r).

[p,q,r,s] | (p or (q and not r) or not s or r)

-------------------------------- --------------|

[0,0,0,0] | 1 |

[0,0,0,1] | 0 |

[0,0,1,0] | 1 |

[0,0,1,1] | 1 |

[0,1,0,0] | 1 |

[0,1,0,1] | 1 |

[0,1,1,0] | 1 |

[0,1,1,1] | 1 |

[1,0,0,0] | 1 |

[1,0,0,1] | 1 |

[1,0,1,0] | 1 |

[1,0,1,1] | 1 |

[1,1,0,0] | 1 |

[1,1,0,1] | 1 |

[1,1,1,0] | 1 |

[1,1,1,1] | 1 |

------------------------------------------ ------

如果有人能帮我把这张表变成析取范式，我会很感激。

【问题讨论】：

这并不容易，第一列中的所有值都等于 0。
为什么所有行都显示 [0,0,0,0] ？您的 table/1 应在符号列表下显示 1/0。

标签： prolog

【解决方案1】：

让我们实现一个通用的真值表评估器，在CDNF 中转换为 Prolog 可评估公式，然后，通过definition，我们将分离每个 minterm：

:- op(900, fy, neg).
:- op(1000, xfy, and).
:- op(1100, xfy, or).

formula(p or (q and neg r) or neg s or r).

cnf(F, CNF) :-
    setof(V, literal(F, V), Ls),
    setof(La, T^(assign(Ls, La), translate(F, La, T), T), CNF).

literal((X or Y), L) :- literal(X,L) ; literal(Y,L).
literal((X and Y), L) :- literal(X,L) ; literal(Y,L).
literal(neg X, L) :- literal(X,L).
literal(L, L) :- atom(L).

assign(Ls, La) :- maplist(assign_literal, Ls, La).
assign_literal(L, L=true).
assign_literal(L, L=false).

translate((X or Y), Ls, (A;B)) :- translate(X, Ls, A), translate(Y, Ls, B).
translate((X and Y), Ls, (A,B)) :- translate(X, Ls, A), translate(Y, Ls, B).
translate(neg X, Ls, \+ A) :- translate(X, Ls, A).
translate(L, Ls, V) :- memberchk(L=V, Ls).

产量：

?- formula(F),cnf(F,CNF),maplist(writeln,CNF).
[p=false,q=false,r=false,s=false]
[p=false,q=false,r=true,s=false]
[p=false,q=false,r=true,s=true]
[p=false,q=true,r=false,s=false]
[p=false,q=true,r=false,s=true]
[p=false,q=true,r=true,s=false]
[p=false,q=true,r=true,s=true]
[p=true,q=false,r=false,s=false]
[p=true,q=false,r=false,s=true]
[p=true,q=false,r=true,s=false]
[p=true,q=false,r=true,s=true]
[p=true,q=true,r=false,s=false]
[p=true,q=true,r=false,s=true]
[p=true,q=true,r=true,s=false]
[p=true,q=true,r=true,s=true]
F = or(p, or(and(q, neg(r)), or(neg(s), r))),
CNF = [[p=false, q=false, r=false, s=false], [p=false, q=false, r=true, s=false], [p=false, q=false, r=true, s=true], [p=false, q=true, r=false, s=false], [p=false, q=true, r=false, ... = ...], [p=false, q=true, ... = ...|...], [p=false, ... = ...|...], [... = ...|...], [...|...]|...].

抱歉输出有点冗长。可以根据更多规格轻松定制。

我使用 neg/1 而不是 not/1 （这已经是一个有效的 Prolog 运算符），只是为了明确区别...

编辑

这里是一个简化，产生一个句法概括。只是 literal/2 和 translate/3 发生了变化，并添加了 translate/2 ：

literal(F, L) :- F =.. [_,X,Y], (literal(X,L) ; literal(Y,L)).
literal(F, L) :- F =.. [_,X], literal(X,L).
literal(L, L) :- atom(L).

translate(and, (,)).
translate(or, (;)).
translate(neg, (\+)).

translate(F, Ls, T) :-
    F =.. [S,X,Y],
    translate(S,O),
    T =.. [O,A,B],
    translate(X, Ls, A), translate(Y, Ls, B).
translate(F, Ls, T) :-
    F =.. [S,X],
    translate(S,O),
    T =.. [O,A],
    translate(X, Ls, A).
translate(F, Ls, T) :- memberchk(F=T, Ls).

更多编辑

上面的代码可以更高效，只是将翻译移出循环

cnf(F, CNF) :-
    setof(V, literal(F, V), Ls),
    translate(F, La, T),
    setof(La, (assign(Ls, La), T), CNF).

需要在最后一个 translate/3 子句中进行小修改：使用 member/2 代替 memberchk

...
translate(F, Ls, T) :- member(F=T, Ls).

时间：用旧版本

4 ?- formula(F),time(cnf(F,CNF)).
% 1,788 inferences, 0.002 CPU in 0.002 seconds (98% CPU, 834727 Lips)

有了新的：

5 ?- formula(F),time(cnf(F,CNF)).
% 282 inferences, 0.001 CPU in 0.001 seconds (99% CPU, 315768 Lips)

大约好 6 倍。

旧有 memberchk：

6 ?- formula(F),time(cnf(F,CNF)).
% 1,083 inferences, 0.002 CPU in 0.002 seconds (98% CPU, 561426 Lips)

嗯，仍然好近 4 倍。

编辑需要更多步骤才能获得真正的 Prolog 公式

cdnf(F, CNDF, Prolog) :-
    cdnf(F, CNDF),  % well, was cnf/2, I renamed to be more precise
    maplist(cj, CNDF, CJs),
    reverse(CJs, [H|T]),
    foldl(dj, T, H, Prolog).

dj(A, B, (A;B)).

cj(A, J) :-
    maplist(tf, A, B),
    reverse(B, [H|T]),
    foldl(cj, T, H, J).
cj(A, B, (A,B)).

tf(S=true,S).
tf(S=false,\+S).

现在，结果更有用了

?- formula(_,F), cdnf(F,_,P).
F = or(p, or(and(q, neg(r)), or(neg(s), r))),
P = (\+p, \+q, \+r, \+s;\+p, \+q, r, \+s;\+p, \+q, r, s;\+p, q, \+r, \+s;\+p, q, \+r, s;\+p, q, r, \+ ...;\+p, q, ..., ...;p, ..., ...;..., ...;...;...)

【讨论】：