Per a expressar fórmules proposicionals en CNF es pot utilizar el
format standard DIMACS. L'arxiu pot començar (no es necessari) amb un
seguit de línies totes elles començant amb la lletra c, que
representen comentaris.

Tot seguir cal introduir una línia de la forma

   p cnf n m 

on n es el nombre de variables i m el nombre de clàusules.  Això
indica que els símbols de predicat seran 1,2,3,...,n (observa que
son nombre consecutius i que el 0 no pot ser utilizat).

A continuació s'expressen les clàusules, cadascuna d'elles en una
línia que acaba en 0, i cada literal de la clàusula separat per un
espai. La negació d'un símbol de predicat n s'expressarà com -n.


Un exemple seria:

c Aixo es un exemple 
c creat per Albert Oliveras
p cnf 5 7
4 2 0
-4 -2 0 
5 0
1 2 3 0
1 -2 5 4 0
1 3 4 0
1 3 -4 0