Solving CNF using Prolog

3.1k views Asked by At

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?

3

There are 3 answers

3
mat On BEST ANSWER

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.

0
Jeremiah Willcock On

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.

0
repeat On

Use !

:- 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.