使用 Prolog 求解 CNF答案

【问题标题】：Solving CNF using Prolog使用 Prolog 求解 CNF
【发布时间】：2011-02-26 21:40:50
【问题描述】：

在学习Prolog的时候，我试着写了一个解决CNF问题的程序（性能不是问题），所以我最终得到了以下代码来解决(!x||y||!z)&&(x||!y||z)&&(x||y||z)&&(!x||!y||z)：

vx(t).
vx(f).
vy(t).
vy(f).
vz(t).
vz(f).

x(X) :- X=t; \+ X=f.
y(Y) :- Y=t; \+ Y=f.
z(Z) :- Z=t; \+ Z=f.
nx(X) :- X=f; \+ X=t.
ny(Y) :- Y=f; \+ Y=t.
nz(Z) :- Z=f; \+ Z=t.

cnf :-
   (nx(X); y(Y); nz(Z)),
   (x(X); ny(Y); z(Z)),
   (x(X); y(Y); z(Z)),
   (nx(X); ny(Y); z(Z)),
   write(X), write(Y), write(Z).

有没有更简单直接的方法来使用这种声明性语言来解决CNF？

【问题讨论】：

标签： prolog conjunctive-normal-form clpb

【解决方案1】：

考虑直接使用内置谓词true/0和false/0，并使用顶层来显示结果（独立地，而不是随后的几个write/1调用，考虑使用format/2）：

boolean(true).
boolean(false).

cnf(X, Y, Z) :-
        maplist(boolean, [X,Y,Z]),
        (\+ X; Y ; \+ Z),
        (   X ; \+ Y ; Z),
        (   X ; Y ; Z),
        (   \+ X ; \+ Y ; Z).

例子：

?- cnf(X, Y, Z).
X = true,
Y = true,
Z = true .

编辑：正如@repeat 所解释的，还要认真研究 CLP(B)：通过布尔值求解约束。

使用 CLP(B)，您可以将上面的整个程序编写为：

:- use_module(library(clpb)).

cnf(X, Y, Z) :-
        sat(~X + Y + ~Z),
        sat(X + ~Y + Z),
        sat(X + Y + Z),
        sat(~X + ~Y + Z).

请参阅@repeat 的答案以了解更多信息。

【讨论】：

我正在使用 Gnu Prolog 1.3，当我运行代码时（在定义 maplist 谓词之后），我得到了一些异常。它可以在其他编译器上运行吗？
添加规则“false :- fail”。如果您的系统还不支持 false/0。最新的 GNU Prolog (1.4) 开发版本、YAP 和 SWI 都有它。
OP在我回答后改了问题，如实翻译了原问题;-)

【解决方案2】：

在 Prolog 中查找“精益定理证明者”（例如 leanTAP 或 leanCoP）以获得简单、简短的定理证明者。这些旨在最大限度地利用 Prolog 功能。尽管像这样的证明者使用一阶逻辑，但 CNF 是其中的一个子集。 Prolog 也有专门的 SAT 求解器，例如 this one。

【讨论】：

【解决方案3】：

使用clpb！

:- use_module(library(clpb))。

要检查某个布尔表达式是否可满足，请使用 sat/1:

% OP: “(!x||y||!z) && (x||!y||z) && (x||y||z) && (!x||!y||z)” ?- sat((~X + Y + ~Z)*(X + ~Y + Z)*(X + Y + Z)*(~X + ~Y + Z))。坐（X=\=X*Y#Z）。

目前还没有具体的解决方案...但是比我们开始使用的术语简单得多的残留物！

要获得具体的真值，请使用labeling/1：

?- sat(X=\=X*Y#Z), labeling([X,Y,Z])。 X = 0，Y = 0，Z = 1 ; X = 0，Y = 1，Z = 1 ; X = 1，Y = 0，Z = 0 ; X = 1，Y = 1，Z = 1。

【讨论】：