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

Question

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

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

Answer 3

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

: - use_module ( библиотека (clpb)).

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

% OP: "(! X || y ||! Z) && (x ||! Y || z) && (x|| y||z) && (! X ||! Y ||z)"?- сат ((~ X + Y + ~ Z) * ​​(X + ~ Y + Z) * ​​(X + Y + Z) * ​​(~ X + ~ Y + Z)).
СБ (Х =\=X*Y#Z).

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

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

? - сат (X=\=X*Y#Z), маркировка ([X,Y,Z]).
   X = 0, Y = 0, Z = 1;  X = 0, Y = 1, Z = 1;  X = 1, Y = 0, Z = 0; Х = 1, Y = 1, Z = 1.