Решение CNF с использованием Пролога - PullRequest
Новая
       39

Решение CNF с использованием Пролога

4 голосов
/ 27 февраля 2011

Во время изучения Пролога я пытался написать программу, решающую проблему с 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 с использованием этого декларативного языка?

Ответы [ 3 ]

5 голосов
/ 27 февраля 2011

Попробуйте использовать встроенные предикаты 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 для получения дополнительной информации об этом.

2 голосов
/ 12 ноября 2015

Используйте ! 

:- <a href="http://www.swi-prolog.org/pldoc/doc_for?object=use_module/1" rel="nofollow">use_module</a>(<a href="http://www.swi-prolog.org/man/clpb.html" rel="nofollow">library(clpb)</a>).

Чтобы проверить, удовлетворяется ли какое-либо логическое выражение, используйте sat/1: 

% OP: "(!x||y||!z) && (x||!y||z) && (x||y||z) && (!x||!y||z)"
?- <a href="http://www.swi-prolog.org/pldoc/doc_for?object=sat/1" rel="nofollow">sat</a>((~X + Y + ~Z)*(X + ~Y + Z)*(X + Y + Z)*(~X + ~Y + Z)).
sat(X=\=X*Y#Z).

Пока нет конкретных решений ... но остаток, который на намного проще , чем термин, с которого мы начали!

Чтобы получить конкретные значения истинности, используйтеlabeling/1: 

?- <a href="http://www.swi-prolog.org/pldoc/doc_for?object=sat/1" rel="nofollow">sat</a>(X=\=X*Y#Z), <a href="http://www.swi-prolog.org/pldoc/doc_for?object=labeling/1" rel="nofollow">labeling</a>([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.
2 голосов
/ 27 февраля 2011

Поищите «Доказатель теорем Бережливости» (например, leanTAP или leanCoP ), чтобы найти простые и короткие средства доказательства теорем в Прологе. Они предназначены для использования функций Prolog с максимальной выгодой. Хотя такие пруверы используют логику первого порядка, CNF является подмножеством этого. Для Пролога также есть специальные SAT-решатели, такие как this .

...