title: Solving CNF using Prolog
body: <p>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 <code>(!x||y||!z)&amp;&amp;(x||!y||z)&amp;&amp;(x||y||z)&amp;&amp;(!x||!y||z)</code>:</p>
  
  <pre><code>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).
  </code></pre>
  
  <p>Is there any simpler and more direct way to solve CNF using this declarative language?</p>