4

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 を解決する、より簡単で直接的な方法はありますか?

4

3 に答える 3

5

組み込みの述語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 .

EDIT : @repeat で説明されているように、CLP(B): Constraint Solving over Booleans も真剣に見てください。

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-26T23:17:27.770 に答える
2

Prolog のシンプルで短い定理証明者については、「無駄のない定理証明者」( leanTAPやLooseCoPなど) を参照してください。これらは、Prolog の機能を最大限に活用するように設計されています。そのような証明者は一次論理を使用しますが、CNF はそのサブセットです。このような Prolog 専用の SAT ソルバーもあります。

于 2011-02-26T21:44:08.070 に答える