用Prolog求解CNF

Question

在学习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问题？

Answer 1

考虑直接使用内置谓词true/0和false/0，并使用toplevel显示结果(独立地，而不是随后的几个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的答案。

Answer 2

在Prolog语言中查找“精益定理证明器”(如leanTAP或leanCoP)，以获得简单、简短的定理证明器。这些都是为了充分利用Prolog特性而设计的。尽管证明者喜欢使用一阶逻辑，但CNF是一阶逻辑的子集。Prolog也有专用的SAT求解器，例如this one。