使用Prolog的

虽然学习Prolog的解决CNF，我试着写一个程序解决CNF问题（性能不是问题），所以我结束了下面的代码来解决(!x||y||!z)&&(x||!y||z)&&(x||y||z)&&(!x||!y||z)：使用Prolog的

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的更简单，更直接的方法？

来源

2011-02-26 banx

考虑直接使用内置的谓词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回答有关它的更多信息。

来源

2011-02-26 23:17:27 mat

我用的是GNU Prolog的1.3，当我运行的代码（定义MAPLIST谓语之后），我得到一些例外。它是否在其他编译器上运行？ – banx 2011-02-27 02:14:01

添加规则“false： - 失败。”如果你的系统还不支持false/0。 GNU Prolog（1.4），YAP和SWI的最新开发版本都拥有它，等等。 – mat 2011-02-28 09:53:03

OP在我的回答后改变了问题，它真实地翻译了原始问题;-) – mat 2015-11-12 18:54:24

在Prolog中查找“精简定理证明器”（例如leanTAP或leanCoP）以获得简单的短定理证明器。这些旨在使用Prolog功能来获得最佳的优势。虽然证明者使用一阶逻辑，但CNF是其中的一个子集。 Prolog也有专门的SAT求解器，例如this one。

来源

2011-02-26 21:44:08

使用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)). 
sat(X=\=X*Y#Z).

没有具体的解决方案（S），但......但残留这很多比术语简单我们开始了！

要进入具体的真值，使用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.

来源

2015-11-12 18:11:48 repeat

回答

相关问题