Solving CNF using Prolog

Question

While learning Prolog, I tried to write a program solving CNF problem (the performance is not an issue), so I ended up with the following code to solve (!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).

Is there any simpler and more direct way to solve CNF using this declarative language?

Answer 1

Consider using the built-in predicates true/0 and false/0 directly, and use the toplevel to display results (independently, instead of several subsequent write/1 calls, consider using 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).

Example:

?- cnf(X, Y, Z).
X = true,
Y = true,
Z = true .

EDIT: As explained by @repeat, also take a serious look at CLP(B): Constraint Solving over Booleans.

With CLP(B), you can write the whole program above as:

:- use_module(library(clpb)).

cnf(X, Y, Z) :-
        sat(~X + Y + ~Z),
        sat(X + ~Y + Z),
        sat(X + Y + Z),
        sat(~X + ~Y + Z).

Please see the answer by @repeat for more information about this.

Answer 2

Look up "lean theorem prover" (such as leanTAP or leanCoP) for simple, short theorem provers in Prolog. Those are designed to use Prolog features to the best possible advantage. Although provers like that use first-order logic, CNF is a subset of that. There are dedicated SAT solvers for Prolog as well, such as this one.

Answer 3

Use clpb!

:- use_module(library(clpb)).

To check if some Boolean expression is satisfiable, use 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).

No concrete solution(s) yet... but a residue that's a lot simpler than the term we started with!

To get to concrete truth values, use 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.