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?

mat · Accepted Answer · 2015-11-13T12:20:56.113

5

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.

edited Nov 13 '15 at 12:20

answered Feb 26 '11 at 23:17

mat

40,498
3
51
78

I am using Gnu Prolog 1.3, when I run the code (after defining the maplist predicate), I get some exception. Does it run on other compilers? – banx Feb 27 '11 at 02:14
2

Add the rule "false :- fail." if your system does not yet support false/0. Recent development version of GNU Prolog (1.4), YAP and SWI all have it, among others. – mat Feb 28 '11 at 09:53
OP changed the question after my answer, which truthfully translated the original question ;-) – mat Nov 12 '15 at 18:54

repeat · Answer 2 · 2016-01-16T01:48:34.450

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.

score 2 · Answer 3 · answered Feb 26 '11 at 21:44

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.

Solving CNF using Prolog

3 Answers3