CNF solution using Prolog

Question

While studying Prolog, I tried to write a program that solves the CNF problem (performance is not a problem), so I decided to use 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 an easier 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 toplevel to display the results (regardless of the next few write/1 calls, use 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 @repeat explained, also take a serious look at CLP (B): Constraint Solving over Booleans.

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

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

See @repeat answer for more on this.

Answer 2

Take a look at the “lean theorem recommendation” (like leanTAP or leanCoP ) for simple, short theoretical predictive functions in Prolog. They are designed to take full advantage of Prolog features. Although such pharmacists use first-order logic, CNF is a subset of this. There are also dedicated SAT solutions for Prolog, such as this one .

Answer 3

Use clpb !

<Preview>: use_module ( library (clpb) ).

To check if any Boolean expression is feasible, sat/1 :

<Preview>% 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)). SB (X = \ = X * Y # Z).

There are no concrete solutions yet ... but the remainder, which is much simpler than the term we started with!

To get specific truth values, use labeling/1 :

<Preview>? - 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.